Metamath Proof Explorer


Theorem nffvmpt1

Description: Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 nfmpt1
 |-  F/_ x ( x e. A |-> B )
2 nfcv
 |-  F/_ x C
3 1 2 nffv
 |-  F/_ x ( ( x e. A |-> B ) ` C )