Theorem nfmpo

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

	Ref	Expression
Hypotheses	nfmpo.1	|- F/_ z A
	nfmpo.2	|- F/_ z B
	nfmpo.3	|- F/_ z C
Assertion	nfmpo	|- F/_ z ( x e. A , y e. B |-> C )

Proof

Step	Hyp	Ref	Expression
1		nfmpo.1	|- F/_ z A
2		nfmpo.2	|- F/_ z B
3		nfmpo.3	|- F/_ z C
4		df-mpo	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = C ) }
5	1	nfcri	|- F/ z x e. A
6	2	nfcri	|- F/ z y e. B
7	5 6	nfan	|- F/ z ( x e. A /\ y e. B )
8	3	nfeq2	|- F/ z w = C
9	7 8	nfan	|- F/ z ( ( x e. A /\ y e. B ) /\ w = C )
10	9	nfoprab	|- F/_ z { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = C ) }
11	4 10	nfcxfr	|- F/_ z ( x e. A , y e. B |-> C )