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 =


Step Hyp Ref Expression
1 noel ¬ x
2 1 bianfi x x A x
3 2 bicomi x A x x
4 3 ineqri A =