Metamath Proof Explorer

Theorem nfmpt1

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008)

Ref Expression
Assertion nfmpt1 
|- F/_ x ( x e. A |-> B )

Proof

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