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 _ z A
nfmpo.2 _ z B
nfmpo.3 _ z C
Assertion nfmpo _ z x A , y B C

Proof

Step Hyp Ref Expression
1 nfmpo.1 _ z A
2 nfmpo.2 _ z B
3 nfmpo.3 _ z C
4 df-mpo x A , y B C = x y w | x A y B w = C
5 1 nfcri z x A
6 2 nfcri z y B
7 5 6 nfan z x A y B
8 3 nfeq2 z w = C
9 7 8 nfan z x A y B w = C
10 9 nfoprab _ z x y w | x A y B w = C
11 4 10 nfcxfr _ z x A , y B C