Theorem nfmpt1 4515

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

Syntax hints:   /\ wa 370   = wceq 1437   e. wcel 1870   F/_wnfc 2577   {copab 4483   |-> cmpt 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-opab 4485  df-mpt 4486

This theorem is referenced by:  nffvmpt1  5889  fvmptss  5974  fvmptdf  5977  mpteqb  5980  fvmptf  5982  ralrnmpt  6046  f1ompt  6059  f1mpt  6177  fliftfun  6220  rdgsucmptf  7154  rdgsucmptnf  7155  frsucmpt  7163  frsucmptn  7164  dom2lem  7616  mapxpen  7744  cnfcom3clem  8209  infxpenc2lem2  8449  dfac8clem  8461  acnlem  8477  fin23lem32  8772  axcc3  8866  ac6num  8907  nfcprod1  13942  yonedalem4b  16112  prdsgsum  17545  cayleyhamilton1  19847  neiptopreu  20080  2ndcdisj  20402  ptcnp  20568  cnmpt11  20609  cnmptk2  20632  xkocnv  20760  utopsnneiplem  21193  restmetu  21516  mbfposr  22485  mbfsup  22497  itg1climres  22549  itg2splitlem  22583  itg2split  22584  itg2cnlem1  22596  nfitg1  22608  dvlipcn  22823  lhop2  22844  dvfsumabs  22852  itgparts  22876  itgsubstlem  22877  itgulm2  23229  lgamgulm2  23826  lgseisenlem2  24141  istrkg2ld  24371  cnlnadjlem5  27559  acunirnmpt2  28102  acunirnmpt2f  28103  aciunf1lem  28104  ofpreima  28108  disjdsct  28123  fpwrelmap  28161  locfinreflem  28506  nfesum1  28700  esumc  28711  esumrnmpt2  28728  esumsup  28749  esumgect  28750  esum2d  28753  sigapildsys  28823  ldgenpisyslem1  28824  voliune  28891  oms0  28958  rrvadd  29111  ballotlem7  29194  cvmcov  29774  trpredlem1  30255  trpredrec  30266  phpreu  31633  poimirlem16  31660  poimirlem19  31663  itg2addnclem  31697  ftc1anclem5  31725  totbndbnd  31825  mzpsubmpt  35294  eq0rabdioph  35328  eqrabdioph  35329  aomclem8  35625  binomcxplemdvbinom  36339  binomcxplemdvsum  36341  binomcxplemnotnn0  36342  refsumcn  36991  refsum2cnlem1  36998  suprnmpt  37061  wessf1ornlem  37082  disjrnmpt2  37086  disjf1o  37089  fompt  37090  disjinfi  37091  fmuldfeqlem1  37232  fmuldfeq  37233  climneg  37261  climdivf  37264  mullimc  37268  idlimc  37278  sumnnodd  37282  neglimc  37300  addlimc  37301  0ellimcdiv  37302  cncfmptssg  37319  cncfshift  37323  cncficcgt0  37338  cncfiooicclem1  37343  dvnmul  37387  dvmptfprod  37389  itgsin0pilem1  37395  ibliccsinexp  37396  itgsinexplem1  37399  itgsinexp  37400  iblspltprt  37419  itgsubsticclem  37421  stoweidlem16  37445  stoweidlem18  37447  stoweidlem19  37448  stoweidlem20  37449  stoweidlem22  37451  stoweidlem23  37452  stoweidlem27  37456  stoweidlem31  37461  stoweidlem32  37462  stoweidlem34  37464  stoweidlem35  37465  stoweidlem36  37466  stoweidlem40  37470  stoweidlem41  37471  stoweidlem42  37472  stoweidlem43  37473  stoweidlem44  37474  stoweidlem45  37475  stoweidlem48  37478  stoweidlem51  37481  stoweidlem55  37485  stoweidlem59  37489  stoweidlem60  37490  stoweidlem62  37492  stoweidlem62OLD  37493  wallispilem5  37500  stirlinglem4  37508  stirlinglem5  37509  stirlinglem8  37512  stirlinglem11  37515  stirlinglem12  37516  stirlinglem13  37517  stirlinglem14  37518  stirlinglem15  37519  stirling  37520  fourierdlem16  37554  fourierdlem21  37559  fourierdlem22  37560  fourierdlem53  37591  fourierdlem68  37606  fourierdlem73  37611  fourierdlem80  37618  fourierdlem89  37627  fourierdlem91  37629  fourierdlem93  37631  fourierdlem103  37641  fourierdlem104  37642  fourierdlem112  37650  fourierdlem115  37653  fourierd  37654  fourierclimd  37655  etransclem48  37714  sge00  37752  sge0revalmpt  37754  sge0f1o  37758  sge0fsummpt  37766  sge0gerp  37771  sge0pnffigt  37772  sge0lefi  37774  sge0ltfirp  37776  sge0resplit  37782  sge0iunmptlemfi  37789  sge0iunmpt  37794  iundjiun  37807  omeiunltfirp  37849  omeiunlempt  37850  aacllem  39301