Metamath Proof Explorer

Theorem in0

Description: The intersection of a class with the empty set is the empty set. Theorem 16 of Suppes p. 26. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion in0 
|- ( A i^i (/) ) = (/)

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. x e. (/)
2 1 bianfi 
 |-  ( x e. (/) <-> ( x e. A /\ x e. (/) ) )
3 2 bicomi 
 |-  ( ( x e. A /\ x e. (/) ) <-> x e. (/) )
4 3 ineqri 
 |-  ( A i^i (/) ) = (/)