Theorem nfmpt1 4536

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

Syntax hints:   /\ wa 369   = wceq 1379   e. wcel 1767   F/_wnfc 2615   {copab 4504   |-> cmpt 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-opab 4506  df-mpt 4507

This theorem is referenced by:  nffvmpt1  5873  fvmptss  5957  fvmptdf  5960  mpteqb  5963  fvmptf  5965  ralrnmpt  6029  f1ompt  6042  f1mpt  6156  fliftfun  6197  rdgsucmptf  7094  rdgsucmptnf  7095  frsucmpt  7103  frsucmptn  7104  dom2lem  7555  mapxpen  7683  cnfcom3clem  8148  cnfcom3clemOLD  8156  infxpenc2lem2  8396  infxpenc2lem2OLD  8400  dfac8clem  8412  acnlem  8428  fin23lem32  8723  axcc3  8817  ac6num  8858  yonedalem4b  15402  prdsgsum  16807  prdsgsumOLD  16808  cayleyhamilton1  19176  neiptopreu  19416  2ndcdisj  19739  ptcnp  19874  cnmpt11  19915  cnmptk2  19938  xkocnv  20066  utopsnneiplem  20501  restmetu  20841  mbfposr  21810  mbfsup  21822  itg1climres  21872  itg2splitlem  21906  itg2split  21907  itg2cnlem1  21919  nfitg1  21931  dvlipcn  22146  lhop2  22167  dvfsumabs  22175  itgparts  22199  itgsubstlem  22200  itgulm2  22554  lgseisenlem2  23369  istrkg2ld  23602  cnlnadjlem5  26682  ofpreima  27195  disjdsct  27209  fpwrelmap  27244  nfesum1  27709  esumc  27718  voliune  27857  oms0  27922  rrvadd  28047  ballotlem7  28130  lgamgulm2  28234  cvmcov  28364  nfcprod1  28635  trpredlem1  28903  trpredrec  28914  itg2addnclem  29659  ftc1anclem5  29687  totbndbnd  29904  mzpsubmpt  30295  eq0rabdioph  30330  eqrabdioph  30331  aomclem8  30627  refsumcn  30999  refsum2cnlem1  31006  suprnmpt  31045  fmuldfeqlem1  31148  fmuldfeq  31149  climneg  31168  climdivf  31170  mullimc  31174  idlimc  31184  sumnnodd  31188  neglimc  31205  addlimc  31206  0ellimcdiv  31207  cncfmptssg  31224  cncfshift  31228  icccncfext  31242  cncficcgt0  31243  cncfiooicclem1  31248  itgsin0pilem1  31283  ibliccsinexp  31284  itgsinexplem1  31287  itgsinexp  31288  iblspltprt  31307  itgsubsticclem  31309  stoweidlem16  31332  stoweidlem18  31334  stoweidlem19  31335  stoweidlem20  31336  stoweidlem22  31338  stoweidlem23  31339  stoweidlem27  31343  stoweidlem31  31347  stoweidlem32  31348  stoweidlem34  31350  stoweidlem35  31351  stoweidlem36  31352  stoweidlem40  31356  stoweidlem41  31357  stoweidlem42  31358  stoweidlem43  31359  stoweidlem44  31360  stoweidlem45  31361  stoweidlem48  31364  stoweidlem51  31367  stoweidlem55  31371  stoweidlem59  31375  stoweidlem60  31376  stoweidlem62  31378  wallispilem5  31385  stirlinglem4  31393  stirlinglem5  31394  stirlinglem8  31397  stirlinglem11  31400  stirlinglem12  31401  stirlinglem13  31402  stirlinglem14  31403  stirlinglem15  31404  stirling  31405  fourierdlem16  31439  fourierdlem21  31444  fourierdlem22  31445  fourierdlem53  31476  fourierdlem68  31491  fourierdlem73  31496  fourierdlem80  31503  fourierdlem89  31512  fourierdlem91  31514  fourierdlem93  31516  fourierdlem103  31526  fourierdlem104  31527  fourierdlem112  31535  fourierdlem115  31538  fourierd  31539  fourierclimd  31540