Theorem nrex1

Description: The class of signed reals is a set. Note that a shorter proof is possible using qsex (and not requiring enrer ), but it would add a dependency on ax-rep . (Contributed by Mario Carneiro, 17-Nov-2014) Extract proof from that of axcnex . (Revised by BJ, 4-Feb-2023) (New usage is discouraged.)

	Ref	Expression
Assertion	nrex1	|- R. e. _V

Proof

Step	Hyp	Ref	Expression
1		df-nr	|- R. = ( ( P. X. P. ) /. ~R )
2		npex	|- P. e. _V
3	2 2	xpex	|- ( P. X. P. ) e. _V
4	3	pwex	|- ~P ( P. X. P. ) e. _V
5		enrer	|- ~R Er ( P. X. P. )
6	5	a1i	|- ( T. -> ~R Er ( P. X. P. ) )
7	6	qsss	|- ( T. -> ( ( P. X. P. ) /. ~R ) C_ ~P ( P. X. P. ) )
8	7	mptru	|- ( ( P. X. P. ) /. ~R ) C_ ~P ( P. X. P. )
9	4 8	ssexi	|- ( ( P. X. P. ) /. ~R ) e. _V
10	1 9	eqeltri	|- R. e. _V