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	|- ( { 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		biidd	|- ( x = y -> ( ph <-> ph ) )
5	4	eqabcbw	|- ( { x | ph } = { x | T. } <-> A. y ( ph <-> y e. { x | T. } ) )
6		dfv2	|- _V = { x | T. }
7	6	eqeq2i	|- ( { x | ph } = _V <-> { x | ph } = { x | T. } )
8		vextru	|- y e. { x | T. }
9	8	tbt	|- ( ph <-> ( ph <-> y e. { x | T. } ) )
10	9	albii	|- ( A. y ph <-> A. y ( ph <-> y e. { x | T. } ) )
11	5 7 10	3bitr4i	|- ( { x | ph } = _V <-> A. y ph )
12	4	ab0w	|- ( { x | ph } = (/) <-> A. y -. ph )
13	11 12	orbi12i	|- ( ( { x | ph } = _V \/ { x | ph } = (/) ) <-> ( A. y ph \/ A. y -. ph ) )
14	3 13	mpbir	|- ( { x | ph } = _V \/ { x | ph } = (/) )