Theorem enrex

Description: The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	enrex	⊢ ~R ∈ V

Proof

Step	Hyp	Ref	Expression
1		npex	⊢ P ∈ V
2	1 1	xpex	⊢ ( P × P ) ∈ V
3	2 2	xpex	⊢ ( ( P × P ) × ( P × P ) ) ∈ V
4		df-enr	⊢ ~R = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) ) ) }
5		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) ) ) } ⊆ ( ( P × P ) × ( P × P ) )
6	4 5	eqsstri	⊢ ~R ⊆ ( ( P × P ) × ( P × P ) )
7	3 6	ssexi	⊢ ~R ∈ V