Theorem nfmpo

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013)

	Ref	Expression
Hypotheses	nfmpo.1	$$⊢\underset{\_}{Ⅎ}zA$$
	nfmpo.2	$$⊢\underset{\_}{Ⅎ}zB$$
	nfmpo.3	$$⊢\underset{\_}{Ⅎ}zC$$
Assertion	nfmpo	$$⊢\underset{\_}{Ⅎ}z\left(x\in A,y\in B⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfmpo.1	$$⊢\underset{\_}{Ⅎ}zA$$
2		nfmpo.2	$$⊢\underset{\_}{Ⅎ}zB$$
3		nfmpo.3	$$⊢\underset{\_}{Ⅎ}zC$$
4		df-mpo	$$⊢\left(x\in A,y\in B⟼C\right)=\left\{⟨⟨x,y⟩,w⟩|\left(\left(x\in A\wedge y\in B\right)\wedge w=C\right)\right\}$$
5	1	nfcri	$$⊢Ⅎzx\in A$$
6	2	nfcri	$$⊢Ⅎzy\in B$$
7	5 6	nfan	$$⊢Ⅎz\left(x\in A\wedge y\in B\right)$$
8	3	nfeq2	$$⊢Ⅎzw=C$$
9	7 8	nfan	$$⊢Ⅎz\left(\left(x\in A\wedge y\in B\right)\wedge w=C\right)$$
10	9	nfoprab	$$⊢\underset{\_}{Ⅎ}z\left\{⟨⟨x,y⟩,w⟩|\left(\left(x\in A\wedge y\in B\right)\wedge w=C\right)\right\}$$
11	4 10	nfcxfr	$$⊢\underset{\_}{Ⅎ}z\left(x\in A,y\in B⟼C\right)$$