applyExtensionality Show Code edit
thm (applyExtensionality ((A x) (B x))
(H (↔ (∈ x A) (∈ x B)))
(= A B)
H
(↔ (∈ x A) (∈ x B))
x generalize
(∀ x (↔ (∈ x A) (∈ x B)))
x A B Extensionality
(→ (∀ x (↔ (∈ x A) (∈ x B))) (= A B))
applyModusPonens
(= A B)
)
edit