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	⊢ ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 𝜑
2		nf3	⊢ ( Ⅎ 𝑦 𝜑 ↔ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 ) )
3	1 2	mpbi	⊢ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 )
4		tbtru	⊢ ( 𝜑 ↔ ( 𝜑 ↔ ⊤ ) )
5		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
6		sbv	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
7	5 6	bitr2i	⊢ ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
8		tru	⊢ ⊤
9		vextru	⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }
10	8 9	2th	⊢ ( ⊤ ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } )
11	7 10	bibi12i	⊢ ( ( 𝜑 ↔ ⊤ ) ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
12	4 11	bitri	⊢ ( 𝜑 ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
13	12	albii	⊢ ( ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
14		dfcleq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
15		dfv2	⊢ V = { 𝑥 ∣ ⊤ }
16	15	eqcomi	⊢ { 𝑥 ∣ ⊤ } = V
17	16	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } ↔ { 𝑥 ∣ 𝜑 } = V )
18	13 14 17	3bitr2i	⊢ ( ∀ 𝑦 𝜑 ↔ { 𝑥 ∣ 𝜑 } = V )
19		equid	⊢ 𝑦 = 𝑦
20	19	nbn3	⊢ ( ¬ 𝜑 ↔ ( 𝜑 ↔ ¬ 𝑦 = 𝑦 ) )
21		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } ↔ [ 𝑦 / 𝑥 ] ¬ 𝑥 = 𝑥 )
22		equid	⊢ 𝑥 = 𝑥
23	22 19	2th	⊢ ( 𝑥 = 𝑥 ↔ 𝑦 = 𝑦 )
24	23	notbii	⊢ ( ¬ 𝑥 = 𝑥 ↔ ¬ 𝑦 = 𝑦 )
25	24	a1i	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑥 ↔ ¬ 𝑦 = 𝑦 ) )
26	25	sbievw	⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝑥 = 𝑥 ↔ ¬ 𝑦 = 𝑦 )
27	21 26	bitr2i	⊢ ( ¬ 𝑦 = 𝑦 ↔ 𝑦 ∈ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } )
28	7 27	bibi12i	⊢ ( ( 𝜑 ↔ ¬ 𝑦 = 𝑦 ) ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } ) )
29	20 28	bitri	⊢ ( ¬ 𝜑 ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } ) )
30	29	albii	⊢ ( ∀ 𝑦 ¬ 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } ) )
31		dfcleq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ¬ 𝑥 = 𝑥 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } ) )
32		dfnul2	⊢ ∅ = { 𝑥 ∣ ¬ 𝑥 = 𝑥 }
33	32	eqcomi	⊢ { 𝑥 ∣ ¬ 𝑥 = 𝑥 } = ∅
34	33	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ¬ 𝑥 = 𝑥 } ↔ { 𝑥 ∣ 𝜑 } = ∅ )
35	30 31 34	3bitr2i	⊢ ( ∀ 𝑦 ¬ 𝜑 ↔ { 𝑥 ∣ 𝜑 } = ∅ )
36	18 35	orbi12i	⊢ ( ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 ) ↔ ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ ) )
37	3 36	mpbi	⊢ ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ )