Metamath Proof Explorer

Theorem eq0rdv

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014)

Ref Expression
Hypothesis eq0rdv.1 
|- ( ph -> -. x e. A )
Assertion eq0rdv 
|- ( ph -> A = (/) )

Proof

Step Hyp Ref Expression
1 eq0rdv.1 
 |-  ( ph -> -. x e. A )
2 1 pm2.21d 
 |-  ( ph -> ( x e. A -> x e. (/) ) )
3 2 ssrdv 
 |-  ( ph -> A C_ (/) )
4 ss0 
 |-  ( A C_ (/) -> A = (/) )
5 3 4 syl 
 |-  ( ph -> A = (/) )