Metamath Proof Explorer


Theorem eldisjeqi

Description: Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021)

Ref Expression
Hypothesis eldisjeqi.1 A = B
Assertion eldisjeqi ElDisj A ElDisj B

Proof

Step Hyp Ref Expression
1 eldisjeqi.1 A = B
2 eldisjeq A = B ElDisj A ElDisj B
3 1 2 ax-mp ElDisj A ElDisj B