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 Gino Giotto, 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 tbtru 
 |-  ( ph <-> ( ph <-> T. ) )
5 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
6 sbv 
 |-  ( [ y / x ] ph <-> ph )
7 5 6 bitr2i 
 |-  ( ph <-> y e. { x | ph } )
8 tru 
 |-  T.
9 vextru 
 |-  y e. { x | T. }
10 8 9 2th 
 |-  ( T. <-> y e. { x | T. } )
11 7 10 bibi12i 
 |-  ( ( ph <-> T. ) <-> ( y e. { x | ph } <-> y e. { x | T. } ) )
12 4 11 bitri 
 |-  ( ph <-> ( y e. { x | ph } <-> y e. { x | T. } ) )
13 12 albii 
 |-  ( A. y ph <-> A. y ( y e. { x | ph } <-> y e. { x | T. } ) )
14 dfcleq 
 |-  ( { x | ph } = { x | T. } <-> A. y ( y e. { x | ph } <-> y e. { x | T. } ) )
15 dfv2 
 |-  _V = { x | T. }
16 15 eqcomi 
 |-  { x | T. } = _V
17 16 eqeq2i 
 |-  ( { x | ph } = { x | T. } <-> { x | ph } = _V )
18 13 14 17 3bitr2i 
 |-  ( A. y ph <-> { x | ph } = _V )
19 equid 
 |-  y = y
20 19 nbn3 
 |-  ( -. ph <-> ( ph <-> -. y = y ) )
21 df-clab 
 |-  ( y e. { x | -. x = x } <-> [ y / x ] -. x = x )
22 equid 
 |-  x = x
23 22 19 2th 
 |-  ( x = x <-> y = y )
24 23 notbii 
 |-  ( -. x = x <-> -. y = y )
25 24 a1i 
 |-  ( x = y -> ( -. x = x <-> -. y = y ) )
26 25 sbievw 
 |-  ( [ y / x ] -. x = x <-> -. y = y )
27 21 26 bitr2i 
 |-  ( -. y = y <-> y e. { x | -. x = x } )
28 7 27 bibi12i 
 |-  ( ( ph <-> -. y = y ) <-> ( y e. { x | ph } <-> y e. { x | -. x = x } ) )
29 20 28 bitri 
 |-  ( -. ph <-> ( y e. { x | ph } <-> y e. { x | -. x = x } ) )
30 29 albii 
 |-  ( A. y -. ph <-> A. y ( y e. { x | ph } <-> y e. { x | -. x = x } ) )
31 dfcleq 
 |-  ( { x | ph } = { x | -. x = x } <-> A. y ( y e. { x | ph } <-> y e. { x | -. x = x } ) )
32 dfnul2 
 |-  (/) = { x | -. x = x }
33 32 eqcomi 
 |-  { x | -. x = x } = (/)
34 33 eqeq2i 
 |-  ( { x | ph } = { x | -. x = x } <-> { x | ph } = (/) )
35 30 31 34 3bitr2i 
 |-  ( A. y -. ph <-> { x | ph } = (/) )
36 18 35 orbi12i 
 |-  ( ( A. y ph \/ A. y -. ph ) <-> ( { x | ph } = _V \/ { x | ph } = (/) ) )
37 3 36 mpbi 
 |-  ( { x | ph } = _V \/ { x | ph } = (/) )