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 |` A ) = ( `' _E |` B ) )
2 1 disjeqd 
 |-  ( A = B -> ( Disj ( `' _E |` A ) <-> Disj ( `' _E |` B ) ) )
3 df-eldisj 
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
4 df-eldisj 
 |-  ( ElDisj B <-> Disj ( `' _E |` B ) )
5 2 3 4 3bitr4g 
 |-  ( A = B -> ( ElDisj A <-> ElDisj B ) )