Theorem nfmpt1 5163

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)

Assertion

Ref	Expression
nfmpt1	⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)

Proof of Theorem nfmpt1

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt 5146	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfopab1 5134	. 2 ⊢ Ⅎ𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
3	1, 2	nfcxfr 2975	1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 398   = wceq 1533   ∈ wcel 2110  Ⅎwnfc 2961  {copab 5127   ↦ cmpt 5145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-opab 5128  df-mpt 5146

This theorem is referenced by:  nffvmpt1  6680  fvmptss  6779  fvmptd3f  6782  mpteqb  6786  fvmptf  6788  ralrnmptw  6859  ralrnmpt  6861  f1ompt  6874  f1mpt  7018  fliftfun  7064  rdgsucmptf  8063  rdgsucmptnf  8064  frsucmpt  8072  frsucmptn  8073  dom2lem  8548  mapxpen  8682  cnfcom3clem  9167  infxpenc2lem2  9445  dfac8clem  9457  acnlem  9473  fin23lem32  9765  axcc3  9859  ac6num  9900  nfcprod1  15263  yonedalem4b  17525  prdsgsum  19100  cayleyhamilton1  21499  neiptopreu  21740  2ndcdisj  22063  ptcnp  22229  cnmpt11  22270  cnmptk2  22293  xkocnv  22421  utopsnneiplem  22855  restmetu  23179  mbfposr  24252  mbfsup  24264  itg1climres  24314  itg2splitlem  24348  itg2split  24349  itg2cnlem1  24361  nfitg1  24373  dvlipcn  24590  lhop2  24611  dvfsumabs  24619  itgparts  24643  itgsubstlem  24644  itgulm2  24996  lgamgulm2  25612  lgseisenlem2  25951  istrkg2ld  26245  cnlnadjlem5  29847  acunirnmpt2  30404  acunirnmpt2f  30405  aciunf1lem  30406  ofpreima  30409  fnpreimac  30415  disjdsct  30437  fpwrelmap  30468  fedgmullem2  31026  locfinreflem  31104  prodindf  31282  nfesum1  31299  esumc  31310  esumrnmpt2  31327  esumsup  31348  esumgect  31349  esum2d  31352  sigapildsys  31421  ldgenpisyslem1  31422  voliune  31488  oms0  31555  rrvadd  31710  ballotlem7  31793  breprexplema  31901  cvmcov  32510  trpredlem1  33066  trpredrec  33077  rdgssun  34658  exrecfnlem  34659  phpreu  34875  matunitlindflem2  34888  poimirlem16  34907  poimirlem19  34910  itg2addnclem  34942  ftc1anclem5  34970  totbndbnd  35066  mzpsubmpt  39338  eq0rabdioph  39371  eqrabdioph  39372  aomclem8  39659  binomcxplemdvbinom  40683  binomcxplemdvsum  40685  binomcxplemnotnn0  40686  refsumcn  41285  refsum2cnlem1  41292  suprnmpt  41428  disjrnmpt2  41447  disjf1o  41450  fompt  41451  disjinfi  41452  choicefi  41461  axccdom  41485  rnmptbd2lem  41518  infnsuprnmpt  41520  rnmptbdlem  41525  rnmptss2  41527  rnmptssbi  41532  supxrleubrnmpt  41677  suprleubrnmpt  41694  infrnmptle  41695  infxrunb3rnmpt  41700  uzub  41703  supminfrnmpt  41717  infxrgelbrnmpt  41728  infrpgernmpt  41739  supminfxrrnmpt  41745  fmuldfeqlem1  41861  fmuldfeq  41862  climneg  41889  climdivf  41891  mullimc  41895  idlimc  41905  sumnnodd  41909  neglimc  41926  addlimc  41927  0ellimcdiv  41928  fnlimfvre  41953  fnlimabslt  41958  climreclmpt  41963  climfveqmpt2  41972  climeldmeqmpt2  41974  climeqmpt  41976  limsupubuz  41992  climinfmpt  41994  limsupubuzmpt  41998  limsupequzmptlem  42007  limsupre2mpt  42009  limsupre3mpt  42013  limsupreuzmpt  42018  liminflelimsuplem  42054  liminfvalxr  42062  liminfvalxrmpt  42065  liminfltlem  42083  liminflbuz2  42094  liminfpnfuz  42095  xlimmnfmpt  42122  xlimpnfmpt  42123  xlimpnfxnegmnf2  42137  cncfmptssg  42151  cncfshift  42155  cncficcgt0  42169  cncfiooicclem1  42174  dvnmul  42226  dvmptfprod  42228  itgsin0pilem1  42233  ibliccsinexp  42234  itgsinexplem1  42237  itgsinexp  42238  iblspltprt  42256  itgsubsticclem  42258  stoweidlem16  42300  stoweidlem18  42302  stoweidlem19  42303  stoweidlem20  42304  stoweidlem22  42306  stoweidlem23  42307  stoweidlem27  42311  stoweidlem31  42315  stoweidlem32  42316  stoweidlem34  42318  stoweidlem35  42319  stoweidlem36  42320  stoweidlem40  42324  stoweidlem41  42325  stoweidlem42  42326  stoweidlem43  42327  stoweidlem44  42328  stoweidlem45  42329  stoweidlem48  42332  stoweidlem51  42335  stoweidlem55  42339  stoweidlem59  42343  stoweidlem60  42344  stoweidlem62  42346  wallispilem5  42353  stirlinglem4  42361  stirlinglem5  42362  stirlinglem8  42365  stirlinglem11  42368  stirlinglem12  42369  stirlinglem13  42370  stirlinglem14  42371  stirlinglem15  42372  stirling  42373  fourierdlem16  42407  fourierdlem21  42412  fourierdlem22  42413  fourierdlem53  42443  fourierdlem68  42458  fourierdlem73  42463  fourierdlem80  42470  fourierdlem89  42479  fourierdlem91  42481  fourierdlem93  42483  fourierdlem103  42493  fourierdlem104  42494  fourierdlem112  42502  fourierdlem115  42505  fourierd  42506  fourierclimd  42507  etransclem48  42566  sge00  42657  sge0revalmpt  42659  sge0f1o  42663  sge0fsummpt  42671  sge0gerp  42676  sge0pnffigt  42677  sge0lefi  42679  sge0ltfirp  42681  sge0resplit  42687  sge0iunmptlemfi  42694  sge0iunmpt  42699  sge0xadd  42716  sge0fsummptf  42717  sge0gtfsumgt  42724  sge0reuz  42728  iundjiun  42741  meaiuninc3v  42765  omeiunltfirp  42800  omeiunlempt  42801  hoicvrrex  42837  ovncvrrp  42845  ovnhoilem1  42882  ovnlecvr2  42891  opnvonmbllem1  42913  iunhoiioolem  42956  pimgtmnf  42999  smfpimltmpt  43022  issmfdmpt  43024  smfconst  43025  smfpimltxrmpt  43034  smflimlem2  43047  smflim  43052  smfpimgtmpt  43056  smfpimgtxrmpt  43059  smfpimcclem  43080  smfpimcc  43081  smflimmpt  43083  smfsupmpt  43088  smfsupxr  43089  smfinfmpt  43092  smflimsuplem2  43094  smflimsuplem7  43099  smflimsupmpt  43102  smfliminfmpt  43105  aacllem  44901