Metamath Proof Explorer

Theorem nfmpo1

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

Ref Expression
Assertion nfmpo1 
|- F/_ x ( x e. A , y e. B |-> C )

Proof

Step Hyp Ref Expression
1 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
2 nfoprab1 
 |-  F/_ x { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
3 1 2 nfcxfr 
 |-  F/_ x ( x e. A , y e. B |-> C )