Metamath Proof Explorer


Theorem nfmpo2

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

Ref Expression
Assertion nfmpo2 _ y x A , y B C

Proof

Step Hyp Ref Expression
1 df-mpo x A , y B C = x y z | x A y B z = C
2 nfoprab2 _ y x y z | x A y B z = C
3 1 2 nfcxfr _ y x A , y B C