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	$$⊢\left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎy\phi$$
2		nf3	$$⊢Ⅎy\phi \leftrightarrow \left(\forall y\phi \vee \forall y\neg \phi \right)$$
3	1 2	mpbi	$$⊢\left(\forall y\phi \vee \forall y\neg \phi \right)$$
4		biidd	$$⊢x=y\to \left(\phi \leftrightarrow \phi \right)$$
5	4	eqabcbw	$$⊢\left\{x|\phi \right\}=\left\{x|\top \right\}\leftrightarrow \forall y\left(\phi \leftrightarrow y\in \left\{x|\top \right\}\right)$$
6		dfv2	$$⊢\mathrm{V}=\left\{x|\top \right\}$$
7	6	eqeq2i	$$⊢\left\{x|\phi \right\}=\mathrm{V}\leftrightarrow \left\{x|\phi \right\}=\left\{x|\top \right\}$$
8		vextru	$$⊢y\in \left\{x|\top \right\}$$
9	8	tbt	$$⊢\phi \leftrightarrow \left(\phi \leftrightarrow y\in \left\{x|\top \right\}\right)$$
10	9	albii	$$⊢\forall y\phi \leftrightarrow \forall y\left(\phi \leftrightarrow y\in \left\{x|\top \right\}\right)$$
11	5 7 10	3bitr4i	$$⊢\left\{x|\phi \right\}=\mathrm{V}\leftrightarrow \forall y\phi$$
12	4	ab0w	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \forall y\neg \phi$$
13	11 12	orbi12i	$$⊢\left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)\leftrightarrow \left(\forall y\phi \vee \forall y\neg \phi \right)$$
14	3 13	mpbir	$$⊢\left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)$$