Theorem nfmpt1 4378

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

Syntax hints:   /\ wa 369   = wceq 1364   e. wcel 1761   F/_wnfc 2564   {copab 4346   e. cmpt 4347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-opab 4348  df-mpt 4349

This theorem is referenced by:  nffvmpt1  5696  fvmptss  5779  fvmptdf  5782  mpteqb  5785  fvmptf  5787  ralrnmpt  5849  f1ompt  5862  f1mpt  5971  fliftfun  6002  rdgsucmptf  6880  rdgsucmptnf  6881  frsucmpt  6889  frsucmptn  6890  dom2lem  7345  mapxpen  7473  cnfcom3clem  7934  cnfcom3clemOLD  7942  infxpenc2lem2  8182  infxpenc2lem2OLD  8186  dfac8clem  8198  acnlem  8214  fin23lem32  8509  axcc3  8603  ac6num  8644  yonedalem4b  15082  prdsgsum  16461  prdsgsumOLD  16462  neiptopreu  18696  2ndcdisj  19019  ptcnp  19154  cnmpt11  19195  cnmptk2  19218  xkocnv  19346  utopsnneiplem  19781  restmetu  20121  mbfposr  21089  mbfsup  21101  itg1climres  21151  itg2splitlem  21185  itg2split  21186  itg2cnlem1  21198  nfitg1  21210  dvlipcn  21425  lhop2  21446  dvfsumabs  21454  itgparts  21478  itgsubstlem  21479  itgulm2  21833  lgseisenlem2  22648  cnlnadjlem5  25410  ofpreima  25919  disjdsct  25933  fpwrelmap  25968  nfesum1  26432  esumc  26441  voliune  26581  rrvadd  26765  ballotlem7  26848  lgamgulm2  26952  cvmcov  27082  nfcprod1  27352  trpredlem1  27620  trpredrec  27631  itg2addnclem  28368  ftc1anclem5  28396  totbndbnd  28613  mzpsubmpt  29004  eq0rabdioph  29040  eqrabdioph  29041  aomclem8  29339  refsumcn  29677  refsum2cnlem1  29684  fmuldfeqlem1  29688  fmuldfeq  29689  climneg  29708  climdivf  29710  itgsin0pilem1  29715  ibliccsinexp  29716  itgsinexplem1  29719  itgsinexp  29720  stoweidlem16  29736  stoweidlem18  29738  stoweidlem19  29739  stoweidlem20  29740  stoweidlem22  29742  stoweidlem23  29743  stoweidlem27  29747  stoweidlem31  29751  stoweidlem32  29752  stoweidlem34  29754  stoweidlem35  29755  stoweidlem36  29756  stoweidlem40  29760  stoweidlem41  29761  stoweidlem42  29762  stoweidlem43  29763  stoweidlem44  29764  stoweidlem45  29765  stoweidlem48  29768  stoweidlem51  29771  stoweidlem55  29775  stoweidlem59  29779  stoweidlem60  29780  stoweidlem62  29782  wallispilem5  29789  stirlinglem4  29797  stirlinglem5  29798  stirlinglem8  29801  stirlinglem11  29804  stirlinglem12  29805  stirlinglem13  29806  stirlinglem14  29807  stirlinglem15  29808  stirling  29809