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

Theorem nfmpt1 4541
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 4512 . 2
2 nfopab1 4518 . 2
31, 2nfcxfr 2617 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  F/_wnfc 2605  {copab 4509  e.cmpt 4510
This theorem is referenced by:  nffvmpt1  5879  fvmptss  5964  fvmptdf  5967  mpteqb  5970  fvmptf  5972  ralrnmpt  6040  f1ompt  6053  f1mpt  6169  fliftfun  6210  rdgsucmptf  7113  rdgsucmptnf  7114  frsucmpt  7122  frsucmptn  7123  dom2lem  7575  mapxpen  7703  cnfcom3clem  8170  cnfcom3clemOLD  8178  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  dfac8clem  8434  acnlem  8450  fin23lem32  8745  axcc3  8839  ac6num  8880  nfcprod1  13717  yonedalem4b  15545  prdsgsum  17007  prdsgsumOLD  17008  cayleyhamilton1  19393  neiptopreu  19634  2ndcdisj  19957  ptcnp  20123  cnmpt11  20164  cnmptk2  20187  xkocnv  20315  utopsnneiplem  20750  restmetu  21090  mbfposr  22059  mbfsup  22071  itg1climres  22121  itg2splitlem  22155  itg2split  22156  itg2cnlem1  22168  nfitg1  22180  dvlipcn  22395  lhop2  22416  dvfsumabs  22424  itgparts  22448  itgsubstlem  22449  itgulm2  22804  lgseisenlem2  23625  istrkg2ld  23858  cnlnadjlem5  26990  ofpreima  27507  disjdsct  27521  fpwrelmap  27556  locfinreflem  27843  nfesum1  28053  esumc  28062  voliune  28201  oms0  28266  rrvadd  28391  ballotlem7  28474  lgamgulm2  28578  cvmcov  28708  trpredlem1  29310  trpredrec  29321  itg2addnclem  30066  ftc1anclem5  30094  totbndbnd  30285  mzpsubmpt  30675  eq0rabdioph  30710  eqrabdioph  30711  aomclem8  31007  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  refsumcn  31405  refsum2cnlem1  31412  suprnmpt  31451  fmuldfeqlem1  31576  fmuldfeq  31577  climneg  31616  climdivf  31618  mullimc  31622  idlimc  31632  sumnnodd  31636  neglimc  31653  addlimc  31654  0ellimcdiv  31655  cncfmptssg  31672  cncfshift  31676  cncficcgt0  31691  cncfiooicclem1  31696  dvnmul  31740  dvmptfprod  31742  itgsin0pilem1  31748  ibliccsinexp  31749  itgsinexplem1  31752  itgsinexp  31753  iblspltprt  31772  itgsubsticclem  31774  stoweidlem16  31798  stoweidlem18  31800  stoweidlem19  31801  stoweidlem20  31802  stoweidlem22  31804  stoweidlem23  31805  stoweidlem27  31809  stoweidlem31  31813  stoweidlem32  31814  stoweidlem34  31816  stoweidlem35  31817  stoweidlem36  31818  stoweidlem40  31822  stoweidlem41  31823  stoweidlem42  31824  stoweidlem43  31825  stoweidlem44  31826  stoweidlem45  31827  stoweidlem48  31830  stoweidlem51  31833  stoweidlem55  31837  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  wallispilem5  31851  stirlinglem4  31859  stirlinglem5  31860  stirlinglem8  31863  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  stirling  31871  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem53  31942  fourierdlem68  31957  fourierdlem73  31962  fourierdlem80  31969  fourierdlem89  31978  fourierdlem91  31980  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem115  32004  fourierd  32005  fourierclimd  32006  etransclem48  32065  aacllem  33216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-opab 4511  df-mpt 4512
  Copyright terms: Public domain W3C validator