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 | ⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-opab | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } | |
2 | nfe1 | ⊢ Ⅎ 𝑦 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) | |
3 | 2 | nfex | ⊢ Ⅎ 𝑦 ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) |
4 | 3 | nfab | ⊢ Ⅎ 𝑦 { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } |
5 | 1 4 | nfcxfr | ⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } |