Theorem nffvmpt1 5565

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

Assertion

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

Distinct variable group:   x, C

Allowed substitution hints:   A( x)   B( x)

Proof of Theorem nffvmpt1

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

Syntax hints:   F/_wnfc 2323   |-> cmpt 4090   ` cfv 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-mpt 4092  df-iota 5215  df-fv 5262

This theorem is referenced by:  fvmptt  5649  fmptco  5724  offval2  6146  ofrfval2  6147  mptelixpg  6788  dom2lem  6826  cc2  7327  fsumf1o  11533  fsum3cvg2  11537  fsumadd  11549  isummulc2  11569  isumshft  11633  fprodf1o  11731  txcnp  14439  cnmpt1t  14453  elplyd  14887