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	$$⊢\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		tbtru	$$⊢\phi \leftrightarrow \left(\phi \leftrightarrow \top \right)$$
5		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
6		sbv	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$
7	5 6	bitr2i	$$⊢\phi \leftrightarrow y\in \left\{x|\phi \right\}$$
8		tru	$$⊢\top$$
9		vextru	$$⊢y\in \left\{x|\top \right\}$$
10	8 9	2th	$$⊢\top \leftrightarrow y\in \left\{x|\top \right\}$$
11	7 10	bibi12i	$$⊢\left(\phi \leftrightarrow \top \right)\leftrightarrow \left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)$$
12	4 11	bitri	$$⊢\phi \leftrightarrow \left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)$$
13	12	albii	$$⊢\forall y\phi \leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)$$
14		dfcleq	$$⊢\left\{x|\phi \right\}=\left\{x|\top \right\}\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)$$
15		dfv2	$$⊢\mathrm{V}=\left\{x|\top \right\}$$
16	15	eqcomi	$$⊢\left\{x|\top \right\}=\mathrm{V}$$
17	16	eqeq2i	$$⊢\left\{x|\phi \right\}=\left\{x|\top \right\}\leftrightarrow \left\{x|\phi \right\}=\mathrm{V}$$
18	13 14 17	3bitr2i	$$⊢\forall y\phi \leftrightarrow \left\{x|\phi \right\}=\mathrm{V}$$
19		equid	$$⊢y=y$$
20	19	nbn3	$$⊢\neg \phi \leftrightarrow \left(\phi \leftrightarrow \neg y=y\right)$$
21		df-clab	$$⊢y\in \left\{x|\neg x=x\right\}\leftrightarrow \left[y/x\right]\neg x=x$$
22		equid	$$⊢x=x$$
23	22 19	2th	$$⊢x=x\leftrightarrow y=y$$
24	23	notbii	$$⊢\neg x=x\leftrightarrow \neg y=y$$
25	24	a1i	$$⊢x=y\to \left(\neg x=x\leftrightarrow \neg y=y\right)$$
26	25	sbievw	$$⊢\left[y/x\right]\neg x=x\leftrightarrow \neg y=y$$
27	21 26	bitr2i	$$⊢\neg y=y\leftrightarrow y\in \left\{x|\neg x=x\right\}$$
28	7 27	bibi12i	$$⊢\left(\phi \leftrightarrow \neg y=y\right)\leftrightarrow \left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\neg x=x\right\}\right)$$
29	20 28	bitri	$$⊢\neg \phi \leftrightarrow \left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\neg x=x\right\}\right)$$
30	29	albii	$$⊢\forall y\neg \phi \leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\neg x=x\right\}\right)$$
31		dfcleq	$$⊢\left\{x|\phi \right\}=\left\{x|\neg x=x\right\}\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\neg x=x\right\}\right)$$
32		dfnul2	$$⊢\varnothing =\left\{x|\neg x=x\right\}$$
33	32	eqcomi	$$⊢\left\{x|\neg x=x\right\}=\varnothing$$
34	33	eqeq2i	$$⊢\left\{x|\phi \right\}=\left\{x|\neg x=x\right\}\leftrightarrow \left\{x|\phi \right\}=\varnothing$$
35	30 31 34	3bitr2i	$$⊢\forall y\neg \phi \leftrightarrow \left\{x|\phi \right\}=\varnothing$$
36	18 35	orbi12i	$$⊢\left(\forall y\phi \vee \forall y\neg \phi \right)\leftrightarrow \left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)$$
37	3 36	mpbi	$$⊢\left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)$$