Theorem nfmpt1 4449

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

Syntax hints:   /\ wa 370   = wceq 1437   e. wcel 1872   F/_wnfc 2550   {copab 4417   |-> cmpt 4418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-opab 4419  df-mpt 4420

This theorem is referenced by:  nffvmpt1  5826  fvmptss  5911  fvmptdf  5914  mpteqb  5917  fvmptf  5919  ralrnmpt  5983  f1ompt  5996  f1mpt  6114  fliftfun  6157  rdgsucmptf  7094  rdgsucmptnf  7095  frsucmpt  7103  frsucmptn  7104  dom2lem  7556  mapxpen  7684  cnfcom3clem  8155  infxpenc2lem2  8395  dfac8clem  8407  acnlem  8423  fin23lem32  8718  axcc3  8812  ac6num  8853  nfcprod1  13900  yonedalem4b  16097  prdsgsum  17546  cayleyhamilton1  19851  neiptopreu  20084  2ndcdisj  20406  ptcnp  20572  cnmpt11  20613  cnmptk2  20636  xkocnv  20764  utopsnneiplem  21197  restmetu  21520  mbfposr  22543  mbfsup  22555  itg1climres  22607  itg2splitlem  22641  itg2split  22642  itg2cnlem1  22654  nfitg1  22666  dvlipcn  22881  lhop2  22902  dvfsumabs  22910  itgparts  22934  itgsubstlem  22935  itgulm2  23299  lgamgulm2  23896  lgseisenlem2  24213  istrkg2ld  24443  cnlnadjlem5  27659  acunirnmpt2  28201  acunirnmpt2f  28202  aciunf1lem  28203  ofpreima  28207  disjdsct  28222  fpwrelmap  28261  locfinreflem  28612  nfesum1  28806  esumc  28817  esumrnmpt2  28834  esumsup  28855  esumgect  28856  esum2d  28859  sigapildsys  28929  ldgenpisyslem1  28930  voliune  28997  oms0  29070  oms0OLD  29074  rrvadd  29230  ballotlem7  29313  ballotlem7OLD  29351  cvmcov  29931  trpredlem1  30412  trpredrec  30423  phpreu  31830  poimirlem16  31857  poimirlem19  31860  itg2addnclem  31894  ftc1anclem5  31922  totbndbnd  32022  mzpsubmpt  35491  eq0rabdioph  35525  eqrabdioph  35526  aomclem8  35826  binomcxplemdvbinom  36609  binomcxplemdvsum  36611  binomcxplemnotnn0  36612  refsumcn  37261  refsum2cnlem1  37268  suprnmpt  37336  wessf1ornlem  37357  disjrnmpt2  37361  disjf1o  37364  fompt  37365  disjinfi  37366  fmuldfeqlem1  37537  fmuldfeq  37538  climneg  37566  climdivf  37569  mullimc  37573  idlimc  37583  sumnnodd  37587  neglimc  37605  addlimc  37606  0ellimcdiv  37607  cncfmptssg  37624  cncfshift  37628  cncficcgt0  37643  cncfiooicclem1  37648  dvnmul  37695  dvmptfprod  37697  itgsin0pilem1  37703  ibliccsinexp  37704  itgsinexplem1  37707  itgsinexp  37708  iblspltprt  37727  itgsubsticclem  37729  stoweidlem16  37753  stoweidlem18  37755  stoweidlem19  37756  stoweidlem20  37757  stoweidlem22  37759  stoweidlem23  37760  stoweidlem27  37764  stoweidlem31  37769  stoweidlem32  37770  stoweidlem34  37772  stoweidlem35  37773  stoweidlem36  37774  stoweidlem40  37778  stoweidlem41  37779  stoweidlem42  37780  stoweidlem43  37781  stoweidlem44  37782  stoweidlem45  37783  stoweidlem48  37786  stoweidlem51  37789  stoweidlem55  37793  stoweidlem59  37797  stoweidlem60  37798  stoweidlem62  37800  stoweidlem62OLD  37801  wallispilem5  37808  stirlinglem4  37816  stirlinglem5  37817  stirlinglem8  37820  stirlinglem11  37823  stirlinglem12  37824  stirlinglem13  37825  stirlinglem14  37826  stirlinglem15  37827  stirling  37828  fourierdlem16  37862  fourierdlem21  37867  fourierdlem22  37868  fourierdlem53  37900  fourierdlem68  37915  fourierdlem73  37920  fourierdlem80  37927  fourierdlem89  37936  fourierdlem91  37938  fourierdlem93  37940  fourierdlem103  37950  fourierdlem104  37951  fourierdlem112  37959  fourierdlem115  37962  fourierd  37963  fourierclimd  37964  etransclem48OLD  38024  etransclem48  38025  sge00  38063  sge0revalmpt  38065  sge0f1o  38069  sge0fsummpt  38077  sge0gerp  38082  sge0pnffigt  38083  sge0lefi  38085  sge0ltfirp  38087  sge0resplit  38093  sge0iunmptlemfi  38100  sge0iunmpt  38105  sge0xadd  38122  sge0fsummptf  38123  sge0gtfsumgt  38130  iundjiun  38143  omeiunltfirp  38185  omeiunlempt  38186  hoicvrrex  38219  ovncvrrp  38227  ovnhoilem1  38264  aacllem  40127