Union-changeVariable Show Code edit
thm (Union-changeVariable ((C x′) (A x′) (C x) (A x)) ()
(↔ (∃ x (∧ (∈ C x) (∈ x A)))
(∃ x′ (∧ (∈ C x′) (∈ x′ A))))
x x′ C MembershipBuilderLL
(→ (= x x′) (↔ (∈ C x) (∈ C x′)))
x x′ A MembershipBuilderRR
(→ (= x x′) (↔ (∈ x A) (∈ x′ A)))
buildConjunctionInConsequent
(→ (= x x′) (↔ (∧ (∈ C x) (∈ x A)) (∧ (∈ C x′) (∈ x′ A))))
ChangeVariableThereExists
(↔ (∃ x (∧ (∈ C x) (∈ x A))) (∃ x′ (∧ (∈ C x′) (∈ x′ A))))
)
edit