Theorem nfmpt1 4747

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)

Assertion

Ref	Expression
nfmpt1	|- F/_ x ( x e. A |-> B )

Proof of Theorem nfmpt1

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt 4730	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
2		nfopab1 4719	. 2 |- F/_ x { <. x , z >. | ( x e. A /\ z = B ) }
3	1, 2	nfcxfr 2762	1 |- F/_ x ( x e. A |-> B )

Syntax hints:   /\ wa 384   = wceq 1483   e. wcel 1990   F/_wnfc 2751   {copab 4712   |-> cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-opab 4713  df-mpt 4730

This theorem is referenced by:  nffvmpt1  6199  fvmptss  6292  fvmptd3f  6295  mpteqb  6299  fvmptf  6301  ralrnmpt  6368  f1ompt  6382  f1mpt  6518  fliftfun  6562  rdgsucmptf  7524  rdgsucmptnf  7525  frsucmpt  7533  frsucmptn  7534  dom2lem  7995  mapxpen  8126  cnfcom3clem  8602  infxpenc2lem2  8843  dfac8clem  8855  acnlem  8871  fin23lem32  9166  axcc3  9260  ac6num  9301  nfcprod1  14640  yonedalem4b  16916  prdsgsum  18377  cayleyhamilton1  20697  neiptopreu  20937  2ndcdisj  21259  ptcnp  21425  cnmpt11  21466  cnmptk2  21489  xkocnv  21617  utopsnneiplem  22051  restmetu  22375  mbfposr  23419  mbfsup  23431  itg1climres  23481  itg2splitlem  23515  itg2split  23516  itg2cnlem1  23528  nfitg1  23540  dvlipcn  23757  lhop2  23778  dvfsumabs  23786  itgparts  23810  itgsubstlem  23811  itgulm2  24163  lgamgulm2  24762  lgseisenlem2  25101  istrkg2ld  25359  cnlnadjlem5  28930  acunirnmpt2  29460  acunirnmpt2f  29461  aciunf1lem  29462  ofpreima  29465  disjdsct  29480  fpwrelmap  29508  locfinreflem  29907  prodindf  30085  nfesum1  30102  esumc  30113  esumrnmpt2  30130  esumsup  30151  esumgect  30152  esum2d  30155  sigapildsys  30225  ldgenpisyslem1  30226  voliune  30292  oms0  30359  rrvadd  30514  ballotlem7  30597  breprexplema  30708  cvmcov  31245  trpredlem1  31727  trpredrec  31738  phpreu  33393  matunitlindflem2  33406  poimirlem16  33425  poimirlem19  33428  itg2addnclem  33461  ftc1anclem5  33489  totbndbnd  33588  mzpsubmpt  37306  eq0rabdioph  37340  eqrabdioph  37341  aomclem8  37631  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  refsumcn  39189  refsum2cnlem1  39196  suprnmpt  39355  wessf1ornlem  39371  disjrnmpt2  39375  disjf1o  39378  fompt  39379  disjinfi  39380  choicefi  39392  axccdom  39416  rnmptbd2lem  39463  infnsuprnmpt  39465  rnmptbdlem  39470  rnmptss2  39472  rnmptssbi  39477  supxrleubrnmpt  39632  suprleubrnmpt  39649  infrnmptle  39650  infxrunb3rnmpt  39655  uzub  39658  supminfrnmpt  39672  infxrgelbrnmpt  39683  infrpgernmpt  39695  supminfxrrnmpt  39701  fmuldfeqlem1  39814  fmuldfeq  39815  climneg  39842  climdivf  39844  mullimc  39848  idlimc  39858  sumnnodd  39862  neglimc  39879  addlimc  39880  0ellimcdiv  39881  fnlimfvre  39906  fnlimabslt  39911  climreclmpt  39916  climfveqmpt2  39925  climeldmeqmpt2  39927  climeqmpt  39929  limsupubuz  39945  climinfmpt  39947  limsupubuzmpt  39951  limsupequzmptlem  39960  limsupre2mpt  39962  limsupre3mpt  39966  limsupreuzmpt  39971  liminflelimsuplem  40007  liminfvalxr  40015  liminfvalxrmpt  40018  liminfltlem  40036  xlimmnfmpt  40069  xlimpnfmpt  40070  cncfmptssg  40083  cncfshift  40087  cncficcgt0  40101  cncfiooicclem1  40106  dvnmul  40158  dvmptfprod  40160  itgsin0pilem1  40165  ibliccsinexp  40166  itgsinexplem1  40169  itgsinexp  40170  iblspltprt  40189  itgsubsticclem  40191  stoweidlem16  40233  stoweidlem18  40235  stoweidlem19  40236  stoweidlem20  40237  stoweidlem22  40239  stoweidlem23  40240  stoweidlem27  40244  stoweidlem31  40248  stoweidlem32  40249  stoweidlem34  40251  stoweidlem35  40252  stoweidlem36  40253  stoweidlem40  40257  stoweidlem41  40258  stoweidlem42  40259  stoweidlem43  40260  stoweidlem44  40261  stoweidlem45  40262  stoweidlem48  40265  stoweidlem51  40268  stoweidlem55  40272  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  wallispilem5  40286  stirlinglem4  40294  stirlinglem5  40295  stirlinglem8  40298  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirling  40306  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem53  40376  fourierdlem68  40391  fourierdlem73  40396  fourierdlem80  40403  fourierdlem89  40412  fourierdlem91  40414  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem115  40438  fourierd  40439  fourierclimd  40440  etransclem48  40499  sge00  40593  sge0revalmpt  40595  sge0f1o  40599  sge0fsummpt  40607  sge0gerp  40612  sge0pnffigt  40613  sge0lefi  40615  sge0ltfirp  40617  sge0resplit  40623  sge0iunmptlemfi  40630  sge0iunmpt  40635  sge0xadd  40652  sge0fsummptf  40653  sge0gtfsumgt  40660  sge0reuz  40664  iundjiun  40677  omeiunltfirp  40733  omeiunlempt  40734  hoicvrrex  40770  ovncvrrp  40778  ovnhoilem1  40815  ovnlecvr2  40824  opnvonmbllem1  40846  iunhoiioolem  40889  pimgtmnf  40932  smfpimltmpt  40955  issmfdmpt  40957  smfconst  40958  smfpimltxrmpt  40967  smflimlem2  40980  smflim  40985  smfpimgtmpt  40989  smfpimgtxrmpt  40992  smfpimcclem  41013  smfpimcc  41014  smflimmpt  41016  smfsupmpt  41021  smfsupxr  41022  smfinfmpt  41025  smflimsuplem2  41027  smflimsuplem7  41032  smflimsupmpt  41035  smfliminfmpt  41038  aacllem  42547