PowerSetAsAbstraction Show Code edit
defthm (PowerSetAsAbstraction object (power A) ((A x z)) ()
(= (power A) (abstract z (∀ x (→ (∈ x z) (∈ x A)))))
result element z′ x′ A PowerSetWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element z′ (∀ x′ (→ (∈ x′ z′) (∈ x′ A)))))))
result element z x A PowerSetWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A)))))))
z′ z x A PowerSet-sub
(→ (= z′ z) (↔ (∀ x (→ (∈ x z′) (∈ x A))) (∀ x (→ (∈ x z) (∈ x A)))))
x z′ A x′ PowerSet-changeVariable
(↔ (∀ x (→ (∈ x z′) (∈ x A))) (∀ x′ (→ (∈ x′ z′) (∈ x′ A))))
transformImplicationBiconditionalLeft
(→ (= z′ z) (↔ (∀ x′ (→ (∈ x′ z′) (∈ x′ A))) (∀ x (→ (∈ x z) (∈ x A)))))
ChangeVariableAbstraction
(= (abstract z′ (∀ x′ (→ (∈ x′ z′) (∈ x′ A)))) (abstract z (∀ x (→ (∈ x z) (∈ x A)))))
)
edit