Theorem nfopab

Description: Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Hypothesis	nfopab.1	⊢ Ⅎ 𝑧 𝜑
Assertion	nfopab	⊢ Ⅎ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		nfopab.1	⊢ Ⅎ 𝑧 𝜑
2		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
3		nfv	⊢ Ⅎ 𝑧 𝑤 = ⟨ 𝑥 , 𝑦 ⟩
4	3 1	nfan	⊢ Ⅎ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
5	4	nfex	⊢ Ⅎ 𝑧 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
6	5	nfex	⊢ Ⅎ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
7	6	nfab	⊢ Ⅎ 𝑧 { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
8	2 7	nfcxfr	⊢ Ⅎ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }