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 

dfenr 
⊢ ~_{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 