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

Theorem nfmpt1 5211
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 5187 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
2 nfopab1 5173 . 2 𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
31, 2nfcxfr 2903 1 𝑥(𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wcel 2106  wnfc 2885  {copab 5165  cmpt 5186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-opab 5166  df-mpt 5187
This theorem is referenced by:  nffvmpt1  6850  fvmptss  6957  fvmptd3f  6960  mpteqb  6964  fvmptf  6966  ralrnmptw  7040  ralrnmpt  7042  f1ompt  7055  f1mpt  7204  fliftfun  7253  rdgsucmptf  8370  rdgsucmptnf  8371  frsucmpt  8380  frsucmptn  8381  dom2lem  8928  mapxpen  9083  cnfcom3clem  9637  ttrclselem1  9657  ttrclselem2  9658  infxpenc2lem2  9952  dfac8clem  9964  acnlem  9980  fin23lem32  10276  axcc3  10370  ac6num  10411  nfcprod1  15785  yonedalem4b  18157  prdsgsum  19749  cayleyhamilton1  22225  neiptopreu  22468  2ndcdisj  22791  ptcnp  22957  cnmpt11  22998  cnmptk2  23021  xkocnv  23149  utopsnneiplem  23583  restmetu  23910  mbfposr  25000  mbfsup  25012  itg1climres  25063  itg2splitlem  25097  itg2split  25098  itg2cnlem1  25110  nfitg1  25122  dvlipcn  25342  lhop2  25363  dvfsumabs  25371  itgparts  25395  itgsubstlem  25396  itgulm2  25752  lgamgulm2  26369  lgseisenlem2  26708  istrkg2ld  27288  cnlnadjlem5  30899  acunirnmpt2  31462  acunirnmpt2f  31463  aciunf1lem  31464  ofpreima  31467  fnpreimac  31473  disjdsct  31500  fpwrelmap  31533  nsgqusf1olem1  32074  nsgqusf1olem3  32076  elrspunidl  32082  fedgmullem2  32202  locfinreflem  32290  prodindf  32491  nfesum1  32508  esumc  32519  esumrnmpt2  32536  esumsup  32557  esumgect  32558  esum2d  32561  sigapildsys  32630  ldgenpisyslem1  32631  voliune  32697  oms0  32766  rrvadd  32921  ballotlem7  33004  breprexplema  33112  cvmcov  33726  rdgssun  35816  exrecfnlem  35817  phpreu  36029  matunitlindflem2  36042  poimirlem16  36061  poimirlem19  36064  itg2addnclem  36096  ftc1anclem5  36122  totbndbnd  36215  pwsgprod  40693  mzpsubmpt  41004  eq0rabdioph  41037  eqrabdioph  41038  aomclem8  41326  binomcxplemdvbinom  42575  binomcxplemdvsum  42577  binomcxplemnotnn0  42578  refsumcn  43177  refsum2cnlem1  43184  disjrnmpt2  43343  disjf1o  43346  fompt  43347  disjinfi  43348  choicefi  43357  axccdom  43379  rnmptbd2lem  43412  infnsuprnmpt  43414  rnmptbdlem  43419  rnmptss2  43421  rnmptssbi  43425  supxrleubrnmpt  43577  suprleubrnmpt  43593  infrnmptle  43594  infxrunb3rnmpt  43599  uzub  43602  supminfrnmpt  43616  infxrgelbrnmpt  43625  infrpgernmpt  43636  supminfxrrnmpt  43642  fmuldfeqlem1  43755  fmuldfeq  43756  climneg  43783  climdivf  43785  mullimc  43789  idlimc  43799  sumnnodd  43803  neglimc  43820  addlimc  43821  0ellimcdiv  43822  fnlimfvre  43847  fnlimabslt  43852  climreclmpt  43857  climfveqmpt2  43866  climeldmeqmpt2  43868  climeqmpt  43870  limsupubuz  43886  climinfmpt  43888  limsupubuzmpt  43892  limsupequzmptlem  43901  limsupre2mpt  43903  limsupre3mpt  43907  limsupreuzmpt  43912  liminflelimsuplem  43948  liminfvalxr  43956  liminfvalxrmpt  43959  liminfltlem  43977  liminflbuz2  43988  liminfpnfuz  43989  xlimmnfmpt  44016  xlimpnfmpt  44017  xlimpnfxnegmnf2  44031  cncfmptssg  44044  cncfshift  44047  cncficcgt0  44061  cncfiooicclem1  44066  dvnmul  44116  dvmptfprod  44118  itgsin0pilem1  44123  ibliccsinexp  44124  itgsinexplem1  44127  itgsinexp  44128  iblspltprt  44146  itgsubsticclem  44148  stoweidlem16  44189  stoweidlem18  44191  stoweidlem19  44192  stoweidlem20  44193  stoweidlem22  44195  stoweidlem23  44196  stoweidlem27  44200  stoweidlem31  44204  stoweidlem32  44205  stoweidlem34  44207  stoweidlem35  44208  stoweidlem36  44209  stoweidlem40  44213  stoweidlem41  44214  stoweidlem42  44215  stoweidlem43  44216  stoweidlem44  44217  stoweidlem45  44218  stoweidlem48  44221  stoweidlem51  44224  stoweidlem55  44228  stoweidlem59  44232  stoweidlem60  44233  stoweidlem62  44235  wallispilem5  44242  stirlinglem4  44250  stirlinglem5  44251  stirlinglem8  44254  stirlinglem11  44257  stirlinglem12  44258  stirlinglem13  44259  stirlinglem14  44260  stirlinglem15  44261  stirling  44262  fourierdlem16  44296  fourierdlem21  44301  fourierdlem22  44302  fourierdlem68  44347  fourierdlem73  44352  fourierdlem80  44359  fourierdlem89  44368  fourierdlem91  44370  fourierdlem93  44372  fourierdlem103  44382  fourierdlem104  44383  fourierdlem112  44391  fourierdlem115  44394  fourierd  44395  fourierclimd  44396  etransclem48  44455  sge00  44549  sge0revalmpt  44551  sge0f1o  44555  sge0fsummpt  44563  sge0gerp  44568  sge0pnffigt  44569  sge0lefi  44571  sge0ltfirp  44573  sge0resplit  44579  sge0iunmptlemfi  44586  sge0iunmpt  44591  sge0xadd  44608  sge0fsummptf  44609  sge0gtfsumgt  44616  sge0reuz  44620  iundjiun  44633  meaiuninc3v  44657  omeiunltfirp  44692  omeiunlempt  44693  hoicvrrex  44729  ovncvrrp  44737  ovnhoilem1  44774  ovnlecvr2  44783  opnvonmbllem1  44805  iunhoiioolem  44848  smfpimltmpt  44919  issmfdmpt  44921  smfconst  44922  smfpimltxrmptf  44931  smflimlem2  44945  smflim  44950  smfpimgtmpt  44954  smfpimgtxrmptf  44957  smfpimcclem  44980  smfpimcc  44981  smflimmpt  44983  smfsupmpt  44988  smfsupxr  44989  smfinfmpt  44992  smflimsuplem2  44994  smflimsuplem7  44999  smflimsupmpt  45002  smfliminfmpt  45005  cfsetsnfsetf  45224  1arymaptfo  46661  2arymaptfo  46672  setrec2mpt  47074  aacllem  47180
  Copyright terms: Public domain W3C validator