Metamath Proof Explorer

Theorem 0pssin

Description: Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020)

Ref Expression
Assertion 0pssin 
|- ( (/) C. ( A i^i B ) <-> E. x ( x e. A /\ x e. B ) )

Proof

Step Hyp Ref Expression
1 0pss 
 |-  ( (/) C. ( A i^i B ) <-> ( A i^i B ) =/= (/) )
2 ndisj 
 |-  ( ( A i^i B ) =/= (/) <-> E. x ( x e. A /\ x e. B ) )
3 1 2 bitri 
 |-  ( (/) C. ( A i^i B ) <-> E. x ( x e. A /\ x e. B ) )