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 )