MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nffvmpt1 Structured version   Visualization version   GIF version

Theorem nffvmpt1 6858
Description: Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
Assertion
Ref Expression
nffvmpt1 𝑥((𝑥𝐴𝐵)‘𝐶)
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem nffvmpt1
StepHypRef Expression
1 nfmpt1 5218 . 2 𝑥(𝑥𝐴𝐵)
2 nfcv 2908 . 2 𝑥𝐶
31, 2nffv 6857 1 𝑥((𝑥𝐴𝐵)‘𝐶)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2888  cmpt 5193  cfv 6501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-iota 6453  df-fv 6509
This theorem is referenced by:  fvmptt  6973  fmptco  7080  offval2f  7637  offval2  7642  ofrfval2  7643  mptelixpg  8880  dom2lem  8939  cantnflem1  9632  acni2  9989  axcc2  10380  seqof2  13973  rlim2  15385  ello1mpt  15410  o1compt  15476  sumfc  15601  fsum  15612  fsumf1o  15615  sumss  15616  fsumcvg2  15619  fsumadd  15632  isummulc2  15654  fsummulc2  15676  fsumrelem  15699  isumshft  15731  zprod  15827  fprod  15831  prodfc  15835  fprodf1o  15836  fprodmul  15850  fproddiv  15851  iserodd  16714  prdsbas3  17370  prdsdsval2  17373  invfuc  17870  yonedalem4b  18172  gsumdixp  20040  evlslem4  21500  elptr2  22941  ptunimpt  22962  ptcldmpt  22981  ptclsg  22982  txcnp  22987  ptcnplem  22988  cnmpt1t  23032  cnmptk2  23053  flfcnp2  23374  voliun  24934  mbfeqalem1  25021  mbfpos  25031  mbfposb  25033  mbfsup  25044  mbfinf  25045  mbflim  25048  i1fposd  25088  isibl2  25147  itgmpt  25163  itgeqa  25194  itggt0  25224  itgcn  25225  limcmpt  25263  lhop2  25395  itgsubstlem  25428  itgsubst  25429  elplyd  25579  coeeq2  25619  dgrle  25620  ulmss  25772  itgulm2  25784  leibpi  26308  rlimcnp  26331  o1cxp  26340  lgamgulmlem2  26395  lgamgulmlem6  26399  fmptcof2  31615  itggt0cn  36177  elrfirn2  41048  eq0rabdioph  41128  monotoddzz  41296  aomclem8  41417  fmuldfeq  43898  vonioo  44997
  Copyright terms: Public domain W3C validator