Theorem nfmpo1

Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013)

	Ref	Expression
Assertion	nfmpo1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A,y\in B⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-mpo	$$⊢\left(x\in A,y\in B⟼C\right)=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\right\}$$
2		nfoprab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=C\right)\right\}$$
3	1 2	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left(x\in A,y\in B⟼C\right)$$