ImplicitMembership Show Code edit
thm (ImplicitMembership ((A x) (B x)) ()
(↔ (∈ A B) (∀ x (→ (= x A) (∈ x B))))
x A B MembershipBuilderRR
(→ (= x A) (↔ (∈ x B) (∈ A B)))
ImplicitForAll
(↔ (∀ x (→ (= x A) (∈ x B))) (∈ A B))
swapBiconditional
(↔ (∈ A B) (∀ x (→ (= x A) (∈ x B))))
)
edit