Theorem nfopabd

Description: Bound-variable hypothesis builder for class abstraction. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Hypotheses	nfopabd.1	⊢ Ⅎ 𝑥 𝜑
	nfopabd.2	⊢ Ⅎ 𝑦 𝜑
	nfopabd.4	⊢ ( 𝜑 → Ⅎ 𝑧 𝜓 )
Assertion	nfopabd	⊢ ( 𝜑 → Ⅎ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		nfopabd.1	⊢ Ⅎ 𝑥 𝜑
2		nfopabd.2	⊢ Ⅎ 𝑦 𝜑
3		nfopabd.4	⊢ ( 𝜑 → Ⅎ 𝑧 𝜓 )
4		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) }
5		nfv	⊢ Ⅎ 𝑤 𝜑
6		nfvd	⊢ ( 𝜑 → Ⅎ 𝑧 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
7	6 3	nfand	⊢ ( 𝜑 → Ⅎ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
8	2 7	nfexd	⊢ ( 𝜑 → Ⅎ 𝑧 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
9	1 8	nfexd	⊢ ( 𝜑 → Ⅎ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
10	5 9	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑧 { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) } )
11	4 10	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )