This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ab0orv

Description: The class abstraction defined by a formula not containing the abstraction variable is either the empty set or the universal class. (Contributed by Mario Carneiro, 29-Aug-2013) (Revised by BJ, 22-Mar-2020) Reduce axiom usage. (Revised by GG, 30-Aug-2024)

Ref Expression
Assertion ab0orv 
|- ( { x | ph } = _V \/ { x | ph } = (/) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ y ph
2 nf3 
 |-  ( F/ y ph <-> ( A. y ph \/ A. y -. ph ) )
3 1 2 mpbi 
 |-  ( A. y ph \/ A. y -. ph )
4 biidd 
 |-  ( x = y -> ( ph <-> ph ) )
5 4 eqabcbw 
 |-  ( { x | ph } = { x | T. } <-> A. y ( ph <-> y e. { x | T. } ) )
6 dfv2 
 |-  _V = { x | T. }
7 6 eqeq2i 
 |-  ( { x | ph } = _V <-> { x | ph } = { x | T. } )
8 vextru 
 |-  y e. { x | T. }
9 8 tbt 
 |-  ( ph <-> ( ph <-> y e. { x | T. } ) )
10 9 albii 
 |-  ( A. y ph <-> A. y ( ph <-> y e. { x | T. } ) )
11 5 7 10 3bitr4i 
 |-  ( { x | ph } = _V <-> A. y ph )
12 4 ab0w 
 |-  ( { x | ph } = (/) <-> A. y -. ph )
13 11 12 orbi12i 
 |-  ( ( { x | ph } = _V \/ { x | ph } = (/) ) <-> ( A. y ph \/ A. y -. ph ) )
14 3 13 mpbir 
 |-  ( { x | ph } = _V \/ { x | ph } = (/) )