Theorem nfmpt1 4258

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

Syntax hints:   /\ wa 359   = wceq 1649   e. wcel 1721   F/_wnfc 2527   {copab 4225   e. cmpt 4226

This theorem is referenced by:  nffvmpt1  5695  fvmptss  5772  fvmptdf  5775  mpteqb  5778  fvmptf  5780  ralrnmpt  5837  f1ompt  5850  f1mpt  5966  fliftfun  5993  rdgsucmptf  6645  rdgsucmptnf  6646  frsucmpt  6654  frsucmptn  6655  dom2lem  7106  mapxpen  7232  cnfcom3clem  7618  infxpenc2lem2  7857  dfac8clem  7869  acnlem  7885  fin23lem32  8180  axcc3  8274  ac6num  8315  nfsum1  12439  yonedalem4b  14328  prdsgsum  15507  neiptopreu  17152  2ndcdisj  17472  ptcnp  17607  cnmpt11  17648  cnmptk2  17671  xkocnv  17799  utopsnneiplem  18230  restmetu  18570  mbfposr  19497  mbfsup  19509  itg1climres  19559  itg2splitlem  19593  itg2split  19594  itg2cnlem1  19606  nfitg1  19618  dvlipcn  19831  lhop2  19852  dvfsumabs  19860  itgparts  19884  itgsubstlem  19885  itgulm2  20278  lgseisenlem2  21087  cnlnadjlem5  23527  ofpreima  24034  disjdsct  24043  nfesum1  24390  esumc  24399  voliune  24538  rrvadd  24663  ballotlem7  24746  lgamgulm2  24773  cvmcov  24903  nfcprod1  25189  trpredlem1  25444  trpredrec  25455  itg2addnclem  26155  totbndbnd  26388  mzpsubmpt  26690  eq0rabdioph  26725  eqrabdioph  26726  aomclem8  27027  refsumcn  27568  refsum2cnlem1  27575  fmuldfeqlem1  27579  fmuldfeq  27580  climneg  27603  climdivf  27605  itgsin0pilem1  27611  ibliccsinexp  27612  itgsinexplem1  27615  itgsinexp  27616  stoweidlem16  27632  stoweidlem18  27634  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem23  27639  stoweidlem27  27643  stoweidlem31  27647  stoweidlem32  27648  stoweidlem34  27650  stoweidlem35  27651  stoweidlem36  27652  stoweidlem40  27656  stoweidlem41  27657  stoweidlem42  27658  stoweidlem43  27659  stoweidlem44  27660  stoweidlem45  27661  stoweidlem48  27664  stoweidlem51  27667  stoweidlem55  27671  stoweidlem59  27675  stoweidlem60  27676  stoweidlem62  27678  wallispilem5  27685  stirlinglem4  27693  stirlinglem5  27694  stirlinglem8  27697  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  stirling  27705

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-opab 4227  df-mpt 4228