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

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 𝜑
2		nf3	⊢ ( Ⅎ 𝑦 𝜑 ↔ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 ) )
3	1 2	mpbi	⊢ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 )
4		biidd	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜑 ) )
5	4	eqabcbw	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } ↔ ∀ 𝑦 ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
6		dfv2	⊢ V = { 𝑥 ∣ ⊤ }
7	6	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } )
8		vextru	⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }
9	8	tbt	⊢ ( 𝜑 ↔ ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
10	9	albii	⊢ ( ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
11	5 7 10	3bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑦 𝜑 )
12	4	ab0w	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ¬ 𝜑 )
13	11 12	orbi12i	⊢ ( ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ ) ↔ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 ) )
14	3 13	mpbir	⊢ ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ )