Theorem nfmpt1 4505

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 4476	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
2		nfopab1 4482	. 2 |- F/_ x { <. x , z >. | ( x e. A /\ z = B ) }
3	1, 2	nfcxfr 2600	1 |- F/_ x ( x e. A |-> B )

Syntax hints:   /\ wa 375   = wceq 1454   e. wcel 1897   F/_wnfc 2589   {copab 4473   |-> cmpt 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-opab 4475  df-mpt 4476

This theorem is referenced by:  nffvmpt1  5895  fvmptss  5980  fvmptdf  5983  mpteqb  5986  fvmptf  5988  ralrnmpt  6053  f1ompt  6066  f1mpt  6186  fliftfun  6229  rdgsucmptf  7171  rdgsucmptnf  7172  frsucmpt  7180  frsucmptn  7181  dom2lem  7634  mapxpen  7763  cnfcom3clem  8235  infxpenc2lem2  8476  dfac8clem  8488  acnlem  8504  fin23lem32  8799  axcc3  8893  ac6num  8934  nfcprod1  14012  yonedalem4b  16209  prdsgsum  17658  cayleyhamilton1  19964  neiptopreu  20197  2ndcdisj  20519  ptcnp  20685  cnmpt11  20726  cnmptk2  20749  xkocnv  20877  utopsnneiplem  21310  restmetu  21633  mbfposr  22656  mbfsup  22668  itg1climres  22720  itg2splitlem  22754  itg2split  22755  itg2cnlem1  22767  nfitg1  22779  dvlipcn  22994  lhop2  23015  dvfsumabs  23023  itgparts  23047  itgsubstlem  23048  itgulm2  23412  lgamgulm2  24009  lgseisenlem2  24326  istrkg2ld  24556  cnlnadjlem5  27772  acunirnmpt2  28310  acunirnmpt2f  28311  aciunf1lem  28312  ofpreima  28316  disjdsct  28331  fpwrelmap  28366  locfinreflem  28715  nfesum1  28909  esumc  28920  esumrnmpt2  28937  esumsup  28958  esumgect  28959  esum2d  28962  sigapildsys  29032  ldgenpisyslem1  29033  voliune  29100  oms0  29173  oms0OLD  29177  rrvadd  29333  ballotlem7  29416  ballotlem7OLD  29454  cvmcov  30034  trpredlem1  30516  trpredrec  30527  phpreu  31973  poimirlem16  32000  poimirlem19  32003  itg2addnclem  32037  ftc1anclem5  32065  totbndbnd  32165  mzpsubmpt  35629  eq0rabdioph  35663  eqrabdioph  35664  aomclem8  35963  binomcxplemdvbinom  36745  binomcxplemdvsum  36747  binomcxplemnotnn0  36748  refsumcn  37390  refsum2cnlem1  37397  suprnmpt  37476  wessf1ornlem  37496  disjrnmpt2  37500  disjf1o  37503  fompt  37504  disjinfi  37505  choicefi  37518  fmuldfeqlem1  37697  fmuldfeq  37698  climneg  37726  climdivf  37729  mullimc  37733  idlimc  37743  sumnnodd  37747  neglimc  37765  addlimc  37766  0ellimcdiv  37767  cncfmptssg  37784  cncfshift  37788  cncficcgt0  37803  cncfiooicclem1  37808  dvnmul  37855  dvmptfprod  37857  itgsin0pilem1  37863  ibliccsinexp  37864  itgsinexplem1  37867  itgsinexp  37868  iblspltprt  37887  itgsubsticclem  37889  stoweidlem16  37913  stoweidlem18  37915  stoweidlem19  37916  stoweidlem20  37917  stoweidlem22  37919  stoweidlem23  37920  stoweidlem27  37924  stoweidlem31  37929  stoweidlem32  37930  stoweidlem34  37932  stoweidlem35  37933  stoweidlem36  37934  stoweidlem40  37938  stoweidlem41  37939  stoweidlem42  37940  stoweidlem43  37941  stoweidlem44  37942  stoweidlem45  37943  stoweidlem48  37946  stoweidlem51  37949  stoweidlem55  37953  stoweidlem59  37957  stoweidlem60  37958  stoweidlem62  37960  stoweidlem62OLD  37961  wallispilem5  37968  stirlinglem4  37976  stirlinglem5  37977  stirlinglem8  37980  stirlinglem11  37983  stirlinglem12  37984  stirlinglem13  37985  stirlinglem14  37986  stirlinglem15  37987  stirling  37988  fourierdlem16  38022  fourierdlem21  38027  fourierdlem22  38028  fourierdlem53  38060  fourierdlem68  38075  fourierdlem73  38080  fourierdlem80  38087  fourierdlem89  38096  fourierdlem91  38098  fourierdlem93  38100  fourierdlem103  38110  fourierdlem104  38111  fourierdlem112  38119  fourierdlem115  38122  fourierd  38123  fourierclimd  38124  etransclem48OLD  38184  etransclem48  38185  sge00  38255  sge0revalmpt  38257  sge0f1o  38261  sge0fsummpt  38269  sge0gerp  38274  sge0pnffigt  38275  sge0lefi  38277  sge0ltfirp  38279  sge0resplit  38285  sge0iunmptlemfi  38292  sge0iunmpt  38297  sge0xadd  38314  sge0fsummptf  38315  sge0gtfsumgt  38322  iundjiun  38335  omeiunltfirp  38377  omeiunlempt  38378  hoicvrrex  38415  ovncvrrp  38423  ovnhoilem1  38460  ovnlecvr2  38469  opnvonmbllem1  38491  aacllem  40812