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 = (/) )