nfoprab3

Description: The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013)

		Ref	Expression
	Assertion	nfoprab3	$⊢ \underline{Ⅎ} z \{⟨⟨x, y⟩, z⟩ \| φ\}$

Step	Hyp	Ref	Expression
1		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
2		nfe1	$⊢ Ⅎ z \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
3	2	nfex	$⊢ Ⅎ z \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
4	3	nfex	$⊢ Ⅎ z \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
5	4	nfab	$⊢ \underline{Ⅎ} z \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
6	1 5	nfcxfr	$⊢ \underline{Ⅎ} z \{⟨⟨x, y⟩, z⟩ \| φ\}$

Metamath Proof Explorer