Metamath Proof Explorer


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 )