Metamath Proof Explorer


Theorem nfopab1

Description: The first 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 nfopab1 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

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