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

Theorem nfmpt1 4887
Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
Assertion
Ref Expression
nfmpt1 𝑥(𝑥𝐴𝐵)

Proof of Theorem nfmpt1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mpt 4870 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
2 nfopab1 4859 . 2 𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
31, 2nfcxfr 2888 1 𝑥(𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1620  wcel 2127  wnfc 2877  {copab 4852  cmpt 4869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-opab 4853  df-mpt 4870
This theorem is referenced by:  nffvmpt1  6348  fvmptss  6442  fvmptd3f  6445  mpteqb  6449  fvmptf  6451  ralrnmpt  6519  f1ompt  6533  f1mpt  6669  fliftfun  6713  rdgsucmptf  7681  rdgsucmptnf  7682  frsucmpt  7690  frsucmptn  7691  dom2lem  8149  mapxpen  8279  cnfcom3clem  8763  infxpenc2lem2  9004  dfac8clem  9016  acnlem  9032  fin23lem32  9329  axcc3  9423  ac6num  9464  nfcprod1  14810  yonedalem4b  17088  prdsgsum  18548  cayleyhamilton1  20870  neiptopreu  21110  2ndcdisj  21432  ptcnp  21598  cnmpt11  21639  cnmptk2  21662  xkocnv  21790  utopsnneiplem  22223  restmetu  22547  mbfposr  23589  mbfsup  23601  itg1climres  23651  itg2splitlem  23685  itg2split  23686  itg2cnlem1  23698  nfitg1  23710  dvlipcn  23927  lhop2  23948  dvfsumabs  23956  itgparts  23980  itgsubstlem  23981  itgulm2  24333  lgamgulm2  24932  lgseisenlem2  25271  istrkg2ld  25529  cnlnadjlem5  29210  acunirnmpt2  29740  acunirnmpt2f  29741  aciunf1lem  29742  ofpreima  29745  disjdsct  29760  fpwrelmap  29788  locfinreflem  30187  prodindf  30365  nfesum1  30382  esumc  30393  esumrnmpt2  30410  esumsup  30431  esumgect  30432  esum2d  30435  sigapildsys  30505  ldgenpisyslem1  30506  voliune  30572  oms0  30639  rrvadd  30794  ballotlem7  30877  breprexplema  30988  cvmcov  31523  trpredlem1  32003  trpredrec  32014  phpreu  33675  matunitlindflem2  33688  poimirlem16  33707  poimirlem19  33710  itg2addnclem  33743  ftc1anclem5  33771  totbndbnd  33870  mzpsubmpt  37777  eq0rabdioph  37811  eqrabdioph  37812  aomclem8  38102  binomcxplemdvbinom  39023  binomcxplemdvsum  39025  binomcxplemnotnn0  39026  refsumcn  39657  refsum2cnlem1  39664  suprnmpt  39823  wessf1ornlem  39839  disjrnmpt2  39843  disjf1o  39846  fompt  39847  disjinfi  39848  choicefi  39860  axccdom  39884  rnmptbd2lem  39931  infnsuprnmpt  39933  rnmptbdlem  39938  rnmptss2  39940  rnmptssbi  39945  supxrleubrnmpt  40099  suprleubrnmpt  40116  infrnmptle  40117  infxrunb3rnmpt  40122  uzub  40125  supminfrnmpt  40139  infxrgelbrnmpt  40150  infrpgernmpt  40162  supminfxrrnmpt  40168  fmuldfeqlem1  40286  fmuldfeq  40287  climneg  40314  climdivf  40316  mullimc  40320  idlimc  40330  sumnnodd  40334  neglimc  40351  addlimc  40352  0ellimcdiv  40353  fnlimfvre  40378  fnlimabslt  40383  climreclmpt  40388  climfveqmpt2  40397  climeldmeqmpt2  40399  climeqmpt  40401  limsupubuz  40417  climinfmpt  40419  limsupubuzmpt  40423  limsupequzmptlem  40432  limsupre2mpt  40434  limsupre3mpt  40438  limsupreuzmpt  40443  liminflelimsuplem  40479  liminfvalxr  40487  liminfvalxrmpt  40490  liminfltlem  40508  xlimmnfmpt  40541  xlimpnfmpt  40542  cncfmptssg  40555  cncfshift  40559  cncficcgt0  40573  cncfiooicclem1  40578  dvnmul  40630  dvmptfprod  40632  itgsin0pilem1  40637  ibliccsinexp  40638  itgsinexplem1  40641  itgsinexp  40642  iblspltprt  40661  itgsubsticclem  40663  stoweidlem16  40705  stoweidlem18  40707  stoweidlem19  40708  stoweidlem20  40709  stoweidlem22  40711  stoweidlem23  40712  stoweidlem27  40716  stoweidlem31  40720  stoweidlem32  40721  stoweidlem34  40723  stoweidlem35  40724  stoweidlem36  40725  stoweidlem40  40729  stoweidlem41  40730  stoweidlem42  40731  stoweidlem43  40732  stoweidlem44  40733  stoweidlem45  40734  stoweidlem48  40737  stoweidlem51  40740  stoweidlem55  40744  stoweidlem59  40748  stoweidlem60  40749  stoweidlem62  40751  wallispilem5  40758  stirlinglem4  40766  stirlinglem5  40767  stirlinglem8  40770  stirlinglem11  40773  stirlinglem12  40774  stirlinglem13  40775  stirlinglem14  40776  stirlinglem15  40777  stirling  40778  fourierdlem16  40812  fourierdlem21  40817  fourierdlem22  40818  fourierdlem53  40848  fourierdlem68  40863  fourierdlem73  40868  fourierdlem80  40875  fourierdlem89  40884  fourierdlem91  40886  fourierdlem93  40888  fourierdlem103  40898  fourierdlem104  40899  fourierdlem112  40907  fourierdlem115  40910  fourierd  40911  fourierclimd  40912  etransclem48  40971  sge00  41065  sge0revalmpt  41067  sge0f1o  41071  sge0fsummpt  41079  sge0gerp  41084  sge0pnffigt  41085  sge0lefi  41087  sge0ltfirp  41089  sge0resplit  41095  sge0iunmptlemfi  41102  sge0iunmpt  41107  sge0xadd  41124  sge0fsummptf  41125  sge0gtfsumgt  41132  sge0reuz  41136  iundjiun  41149  meaiuninc3v  41173  omeiunltfirp  41208  omeiunlempt  41209  hoicvrrex  41245  ovncvrrp  41253  ovnhoilem1  41290  ovnlecvr2  41299  opnvonmbllem1  41321  iunhoiioolem  41364  pimgtmnf  41407  smfpimltmpt  41430  issmfdmpt  41432  smfconst  41433  smfpimltxrmpt  41442  smflimlem2  41455  smflim  41460  smfpimgtmpt  41464  smfpimgtxrmpt  41467  smfpimcclem  41488  smfpimcc  41489  smflimmpt  41491  smfsupmpt  41496  smfsupxr  41497  smfinfmpt  41500  smflimsuplem2  41502  smflimsuplem7  41507  smflimsupmpt  41510  smfliminfmpt  41513  aacllem  43029
  Copyright terms: Public domain W3C validator