This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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