Metamath Proof Explorer


Theorem int0el

Description: The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion int0el
|- ( (/) e. A -> |^| A = (/) )

Proof

Step Hyp Ref Expression
1 intss1
 |-  ( (/) e. A -> |^| A C_ (/) )
2 0ss
 |-  (/) C_ |^| A
3 2 a1i
 |-  ( (/) e. A -> (/) C_ |^| A )
4 1 3 eqssd
 |-  ( (/) e. A -> |^| A = (/) )