buildMembershipRRInConsequent Show Code edit
thm (buildMembershipRRInConsequent ()
(H (→ antecedent (= A0 A1)))
(→ antecedent (↔ (∈ A0 B) (∈ A1 B)))
H
(→ antecedent (= A0 A1))
A0 A1 B MembershipBuilderRR
(→ (= A0 A1) (↔ (∈ A0 B) (∈ A1 B)))
applySyllogism
(→ antecedent (↔ (∈ A0 B) (∈ A1 B)))
)
edit