Metamath Proof Explorer


Theorem eldisjeq

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

Ref Expression
Assertion eldisjeq A = B ElDisj A ElDisj B

Proof

Step Hyp Ref Expression
1 reseq2 A = B E -1 A = E -1 B
2 1 disjeqd A = B Disj E -1 A Disj E -1 B
3 df-eldisj ElDisj A Disj E -1 A
4 df-eldisj ElDisj B Disj E -1 B
5 2 3 4 3bitr4g A = B ElDisj A ElDisj B