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

Theorem nffvmpt1 6657
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 5140 . 2 𝑥(𝑥𝐴𝐵)
2 nfcv 2973 . 2 𝑥𝐶
31, 2nffv 6656 1 𝑥((𝑥𝐴𝐵)‘𝐶)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2957  cmpt 5122  cfv 6331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-mpt 5123  df-iota 6290  df-fv 6339
This theorem is referenced by:  fvmptt  6764  fmptco  6867  offval2f  7399  offval2  7404  ofrfval2  7405  mptelixpg  8477  dom2lem  8527  cantnflem1  9130  acni2  9450  axcc2  9837  seqof2  13413  rlim2  14833  ello1mpt  14858  o1compt  14924  sumfc  15046  fsum  15057  fsumf1o  15060  sumss  15061  fsumcvg2  15064  fsumadd  15076  isummulc2  15097  fsummulc2  15119  fsumrelem  15142  isumshft  15174  zprod  15271  fprod  15275  prodfc  15279  fprodf1o  15280  fprodmul  15294  fproddiv  15295  iserodd  16150  prdsbas3  16733  prdsdsval2  16736  invfuc  17223  yonedalem4b  17505  gsumdixp  19338  evlslem4  20264  elptr2  22158  ptunimpt  22179  ptcldmpt  22198  ptclsg  22199  txcnp  22204  ptcnplem  22205  cnmpt1t  22249  cnmptk2  22270  flfcnp2  22591  voliun  24137  mbfeqalem1  24224  mbfpos  24234  mbfposb  24236  mbfsup  24247  mbfinf  24248  mbflim  24251  i1fposd  24290  isibl2  24349  itgmpt  24365  itgeqa  24396  itggt0  24426  itgcn  24427  limcmpt  24465  lhop2  24597  itgsubstlem  24630  itgsubst  24631  elplyd  24778  coeeq2  24818  dgrle  24819  ulmss  24971  itgulm2  24983  leibpi  25507  rlimcnp  25530  o1cxp  25539  lgamgulmlem2  25594  lgamgulmlem6  25598  fmptcof2  30389  itggt0cn  35003  elrfirn2  39430  eq0rabdioph  39510  monotoddzz  39677  aomclem8  39798  fmuldfeq  42016  vonioo  43112
  Copyright terms: Public domain W3C validator