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

Theorem nfmpt1 4669
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 4639 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
2 nfopab1 4645 . 2 𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
31, 2nfcxfr 2748 1 𝑥(𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1976  wnfc 2737  {copab 4636  cmpt 4637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-opab 4638  df-mpt 4639
This theorem is referenced by:  nffvmpt1  6096  fvmptss  6186  fvmptdf  6189  mpteqb  6192  fvmptf  6194  ralrnmpt  6261  f1ompt  6275  f1mpt  6397  fliftfun  6440  rdgsucmptf  7388  rdgsucmptnf  7389  frsucmpt  7397  frsucmptn  7398  dom2lem  7858  mapxpen  7988  cnfcom3clem  8462  infxpenc2lem2  8703  dfac8clem  8715  acnlem  8731  fin23lem32  9026  axcc3  9120  ac6num  9161  nfcprod1  14425  yonedalem4b  16685  prdsgsum  18146  cayleyhamilton1  20458  neiptopreu  20689  2ndcdisj  21011  ptcnp  21177  cnmpt11  21218  cnmptk2  21241  xkocnv  21369  utopsnneiplem  21803  restmetu  22126  mbfposr  23142  mbfsup  23154  itg1climres  23204  itg2splitlem  23238  itg2split  23239  itg2cnlem1  23251  nfitg1  23263  dvlipcn  23478  lhop2  23499  dvfsumabs  23507  itgparts  23531  itgsubstlem  23532  itgulm2  23884  lgamgulm2  24479  lgseisenlem2  24818  istrkg2ld  25076  cnlnadjlem5  28120  acunirnmpt2  28648  acunirnmpt2f  28649  aciunf1lem  28650  ofpreima  28654  disjdsct  28669  fpwrelmap  28702  locfinreflem  29041  nfesum1  29235  esumc  29246  esumrnmpt2  29263  esumsup  29284  esumgect  29285  esum2d  29288  sigapildsys  29358  ldgenpisyslem1  29359  voliune  29425  oms0  29492  rrvadd  29647  ballotlem7  29730  cvmcov  30305  trpredlem1  30777  trpredrec  30788  phpreu  32359  matunitlindflem2  32372  poimirlem16  32391  poimirlem19  32394  itg2addnclem  32427  ftc1anclem5  32455  totbndbnd  32554  mzpsubmpt  36120  eq0rabdioph  36154  eqrabdioph  36155  aomclem8  36445  binomcxplemdvbinom  37370  binomcxplemdvsum  37372  binomcxplemnotnn0  37373  refsumcn  38008  refsum2cnlem1  38015  suprnmpt  38146  wessf1ornlem  38162  disjrnmpt2  38166  disjf1o  38169  fompt  38170  disjinfi  38171  choicefi  38183  axccdom  38207  fmuldfeqlem1  38446  fmuldfeq  38447  climneg  38474  climdivf  38476  mullimc  38480  idlimc  38490  sumnnodd  38494  neglimc  38511  addlimc  38512  0ellimcdiv  38513  fnlimfvre  38538  fnlimabslt  38543  cncfmptssg  38552  cncfshift  38556  cncficcgt0  38571  cncfiooicclem1  38576  dvnmul  38630  dvmptfprod  38632  itgsin0pilem1  38638  ibliccsinexp  38639  itgsinexplem1  38642  itgsinexp  38643  iblspltprt  38662  itgsubsticclem  38664  stoweidlem16  38706  stoweidlem18  38708  stoweidlem19  38709  stoweidlem20  38710  stoweidlem22  38712  stoweidlem23  38713  stoweidlem27  38717  stoweidlem31  38721  stoweidlem32  38722  stoweidlem34  38724  stoweidlem35  38725  stoweidlem36  38726  stoweidlem40  38730  stoweidlem41  38731  stoweidlem42  38732  stoweidlem43  38733  stoweidlem44  38734  stoweidlem45  38735  stoweidlem48  38738  stoweidlem51  38741  stoweidlem55  38745  stoweidlem59  38749  stoweidlem60  38750  stoweidlem62  38752  wallispilem5  38759  stirlinglem4  38767  stirlinglem5  38768  stirlinglem8  38771  stirlinglem11  38774  stirlinglem12  38775  stirlinglem13  38776  stirlinglem14  38777  stirlinglem15  38778  stirling  38779  fourierdlem16  38813  fourierdlem21  38818  fourierdlem22  38819  fourierdlem53  38849  fourierdlem68  38864  fourierdlem73  38869  fourierdlem80  38876  fourierdlem89  38885  fourierdlem91  38887  fourierdlem93  38889  fourierdlem103  38899  fourierdlem104  38900  fourierdlem112  38908  fourierdlem115  38911  fourierd  38912  fourierclimd  38913  etransclem48  38972  sge00  39066  sge0revalmpt  39068  sge0f1o  39072  sge0fsummpt  39080  sge0gerp  39085  sge0pnffigt  39086  sge0lefi  39088  sge0ltfirp  39090  sge0resplit  39096  sge0iunmptlemfi  39103  sge0iunmpt  39108  sge0xadd  39125  sge0fsummptf  39126  sge0gtfsumgt  39133  sge0reuz  39137  iundjiun  39150  omeiunltfirp  39206  omeiunlempt  39207  hoicvrrex  39243  ovncvrrp  39251  ovnhoilem1  39288  ovnlecvr2  39297  opnvonmbllem1  39319  iunhoiioolem  39363  pimgtmnf  39406  smfpimltmpt  39430  issmfdmpt  39432  smfconst  39433  smfpimltxrmpt  39442  smflimlem2  39455  smflim  39460  smfpimgtmpt  39464  smfpimgtxrmpt  39467  aacllem  42312
  Copyright terms: Public domain W3C validator