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 )