Theorem nfmpt1 4393

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

Syntax hints:   /\ wa 369   = wceq 1369   e. wcel 1756   F/_wnfc 2575   {copab 4361   e. cmpt 4362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-opab 4363  df-mpt 4364

This theorem is referenced by:  nffvmpt1  5711  fvmptss  5794  fvmptdf  5797  mpteqb  5800  fvmptf  5802  ralrnmpt  5864  f1ompt  5877  f1mpt  5986  fliftfun  6017  rdgsucmptf  6896  rdgsucmptnf  6897  frsucmpt  6905  frsucmptn  6906  dom2lem  7361  mapxpen  7489  cnfcom3clem  7950  cnfcom3clemOLD  7958  infxpenc2lem2  8198  infxpenc2lem2OLD  8202  dfac8clem  8214  acnlem  8230  fin23lem32  8525  axcc3  8619  ac6num  8660  yonedalem4b  15098  prdsgsum  16483  prdsgsumOLD  16484  neiptopreu  18749  2ndcdisj  19072  ptcnp  19207  cnmpt11  19248  cnmptk2  19271  xkocnv  19399  utopsnneiplem  19834  restmetu  20174  mbfposr  21142  mbfsup  21154  itg1climres  21204  itg2splitlem  21238  itg2split  21239  itg2cnlem1  21251  nfitg1  21263  dvlipcn  21478  lhop2  21499  dvfsumabs  21507  itgparts  21531  itgsubstlem  21532  itgulm2  21886  lgseisenlem2  22701  cnlnadjlem5  25487  ofpreima  25996  disjdsct  26010  fpwrelmap  26045  nfesum1  26508  esumc  26517  voliune  26657  oms0  26722  rrvadd  26847  ballotlem7  26930  lgamgulm2  27034  cvmcov  27164  nfcprod1  27435  trpredlem1  27703  trpredrec  27714  itg2addnclem  28455  ftc1anclem5  28483  totbndbnd  28700  mzpsubmpt  29091  eq0rabdioph  29127  eqrabdioph  29128  aomclem8  29426  refsumcn  29764  refsum2cnlem1  29771  fmuldfeqlem1  29775  fmuldfeq  29776  climneg  29795  climdivf  29797  itgsin0pilem1  29802  ibliccsinexp  29803  itgsinexplem1  29806  itgsinexp  29807  stoweidlem16  29823  stoweidlem18  29825  stoweidlem19  29826  stoweidlem20  29827  stoweidlem22  29829  stoweidlem23  29830  stoweidlem27  29834  stoweidlem31  29838  stoweidlem32  29839  stoweidlem34  29841  stoweidlem35  29842  stoweidlem36  29843  stoweidlem40  29847  stoweidlem41  29848  stoweidlem42  29849  stoweidlem43  29850  stoweidlem44  29851  stoweidlem45  29852  stoweidlem48  29855  stoweidlem51  29858  stoweidlem55  29862  stoweidlem59  29866  stoweidlem60  29867  stoweidlem62  29869  wallispilem5  29876  stirlinglem4  29884  stirlinglem5  29885  stirlinglem8  29888  stirlinglem11  29891  stirlinglem12  29892  stirlinglem13  29893  stirlinglem14  29894  stirlinglem15  29895  stirling  29896