Metamath Proof Explorer

Theorem disjeccnvep

Description: Property of the epsilon relation. (Contributed by Peter Mazsa, 27-Apr-2020)

Ref Expression
Assertion disjeccnvep 
|- ( ( A e. V /\ B e. W ) -> ( ( [ A ] `' _E i^i [ B ] `' _E ) = (/) <-> ( A i^i B ) = (/) ) )

Proof

Step Hyp Ref Expression
1 eccnvep 
 |-  ( A e. V -> [ A ] `' _E = A )
2 eccnvep 
 |-  ( B e. W -> [ B ] `' _E = B )
3 1 2 ineqan12d 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] `' _E i^i [ B ] `' _E ) = ( A i^i B ) )
4 3 eqeq1d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] `' _E i^i [ B ] `' _E ) = (/) <-> ( A i^i B ) = (/) ) )