Theorem nfoprab

Description: Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013)

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

Proof

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