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 𝐴 = 𝐵
Assertion eldisjeqi ( ElDisj 𝐴 ↔ ElDisj 𝐵 )

Proof

Step Hyp Ref Expression
1 eldisjeqi.1 𝐴 = 𝐵
2 eldisjeq ( 𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵 ) )
3 1 2 ax-mp ( ElDisj 𝐴 ↔ ElDisj 𝐵 )