Metamath Proof Explorer


Theorem nfopab2

Description: The second abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion nfopab2 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

Step Hyp Ref Expression
1 df-opab { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
2 nfe1 𝑦𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
3 2 nfex 𝑦𝑥𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
4 3 nfab 𝑦 { 𝑧 ∣ ∃ 𝑥𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
5 1 4 nfcxfr 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }