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

Theorem nffvmpt1 6674
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 5155 . 2 𝑥(𝑥𝐴𝐵)
2 nfcv 2974 . 2 𝑥𝐶
31, 2nffv 6673 1 𝑥((𝑥𝐴𝐵)‘𝐶)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2958  cmpt 5137  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-iota 6307  df-fv 6356
This theorem is referenced by:  fvmptt  6780  fmptco  6883  offval2f  7410  offval2  7415  ofrfval2  7416  mptelixpg  8487  dom2lem  8537  cantnflem1  9140  acni2  9460  axcc2  9847  seqof2  13416  rlim2  14841  ello1mpt  14866  o1compt  14932  sumfc  15054  fsum  15065  fsumf1o  15068  sumss  15069  fsumcvg2  15072  fsumadd  15084  isummulc2  15105  fsummulc2  15127  fsumrelem  15150  isumshft  15182  zprod  15279  fprod  15283  prodfc  15287  fprodf1o  15288  fprodmul  15302  fproddiv  15303  iserodd  16160  prdsbas3  16742  prdsdsval2  16745  invfuc  17232  yonedalem4b  17514  gsumdixp  19288  evlslem4  20216  elptr2  22110  ptunimpt  22131  ptcldmpt  22150  ptclsg  22151  txcnp  22156  ptcnplem  22157  cnmpt1t  22201  cnmptk2  22222  flfcnp2  22543  voliun  24082  mbfeqalem1  24169  mbfpos  24179  mbfposb  24181  mbfsup  24192  mbfinf  24193  mbflim  24196  i1fposd  24235  isibl2  24294  itgmpt  24310  itgeqa  24341  itggt0  24369  itgcn  24370  limcmpt  24408  lhop2  24539  itgsubstlem  24572  itgsubst  24573  elplyd  24719  coeeq2  24759  dgrle  24760  ulmss  24912  itgulm2  24924  leibpi  25447  rlimcnp  25470  o1cxp  25479  lgamgulmlem2  25534  lgamgulmlem6  25538  fmptcof2  30330  itggt0cn  34845  elrfirn2  39171  eq0rabdioph  39251  monotoddzz  39418  aomclem8  39539  fmuldfeq  41740  vonioo  42841
  Copyright terms: Public domain W3C validator