Metamath Proof Explorer

Theorem vdif0

Description: Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003)

Ref Expression
Assertion vdif0 
|- ( A = _V <-> ( _V \ A ) = (/) )

Proof

Step Hyp Ref Expression
1 vss 
 |-  ( _V C_ A <-> A = _V )
2 ssdif0 
 |-  ( _V C_ A <-> ( _V \ A ) = (/) )
3 1 2 bitr3i 
 |-  ( A = _V <-> ( _V \ A ) = (/) )