buildMembershipRR Show Code edit
thm (buildMembershipRR () (H (= A0 A1)) (↔ (∈ A0 B) (∈ A1 B))
H
(= A0 A1)
A0 A1 B MembershipBuilderRR
(→ (= A0 A1) (↔ (∈ A0 B) (∈ A1 B)))
applyModusPonens
(↔ (∈ A0 B) (∈ A1 B))
)
edit