Metamath Proof Explorer


Theorem nfmpt

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013)

Ref Expression
Hypotheses nfmpt.1
|- F/_ x A
nfmpt.2
|- F/_ x B
Assertion nfmpt
|- F/_ x ( y e. A |-> B )

Proof

Step Hyp Ref Expression
1 nfmpt.1
 |-  F/_ x A
2 nfmpt.2
 |-  F/_ x B
3 df-mpt
 |-  ( y e. A |-> B ) = { <. y , z >. | ( y e. A /\ z = B ) }
4 1 nfcri
 |-  F/ x y e. A
5 2 nfeq2
 |-  F/ x z = B
6 4 5 nfan
 |-  F/ x ( y e. A /\ z = B )
7 6 nfopab
 |-  F/_ x { <. y , z >. | ( y e. A /\ z = B ) }
8 3 7 nfcxfr
 |-  F/_ x ( y e. A |-> B )