PowerSet-changeVariable Show Code edit
thm (PowerSet-changeVariable ((C x′) (A x′) (C x) (A x)) ()
(↔ (∀ x (→ (∈ x C) (∈ x A)))
(∀ x′ (→ (∈ x′ C) (∈ x′ A))))
x x′ C MembershipBuilderRR
(→ (= x x′) (↔ (∈ x C) (∈ x′ C)))
x x′ A MembershipBuilderRR
(→ (= x x′) (↔ (∈ x A) (∈ x′ A)))
buildImplicationInConsequent
(→ (= x x′) (↔ (→ (∈ x C) (∈ x A)) (→ (∈ x′ C) (∈ x′ A))))
ChangeVariableForAll
(↔ (∀ x (→ (∈ x C) (∈ x A))) (∀ x′ (→ (∈ x′ C) (∈ x′ A))))
)
edit