Theorem nfmpt1 5133

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 5116	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfopab1 5104	. 2 ⊢ Ⅎ𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
3	1, 2	nfcxfr 2917	1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Ⅎwnfc 2899  {copab 5097   ↦ cmpt 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-opab 5098  df-mpt 5116

This theorem is referenced by:  nffvmpt1  6673  fvmptss  6775  fvmptd3f  6778  mpteqb  6782  fvmptf  6784  ralrnmptw  6856  ralrnmpt  6858  f1ompt  6871  f1mpt  7016  fliftfun  7064  rdgsucmptf  8079  rdgsucmptnf  8080  frsucmpt  8088  frsucmptn  8089  dom2lem  8572  mapxpen  8710  cnfcom3clem  9206  infxpenc2lem2  9485  dfac8clem  9497  acnlem  9513  fin23lem32  9809  axcc3  9903  ac6num  9944  nfcprod1  15317  yonedalem4b  17597  prdsgsum  19174  cayleyhamilton1  21597  neiptopreu  21838  2ndcdisj  22161  ptcnp  22327  cnmpt11  22368  cnmptk2  22391  xkocnv  22519  utopsnneiplem  22953  restmetu  23277  mbfposr  24357  mbfsup  24369  itg1climres  24419  itg2splitlem  24453  itg2split  24454  itg2cnlem1  24466  nfitg1  24478  dvlipcn  24698  lhop2  24719  dvfsumabs  24727  itgparts  24751  itgsubstlem  24752  itgulm2  25108  lgamgulm2  25725  lgseisenlem2  26064  istrkg2ld  26358  cnlnadjlem5  29958  acunirnmpt2  30525  acunirnmpt2f  30526  aciunf1lem  30527  ofpreima  30530  fnpreimac  30536  disjdsct  30563  fpwrelmap  30596  nsgqusf1olem1  31123  nsgqusf1olem3  31125  elrspunidl  31131  fedgmullem2  31236  locfinreflem  31315  prodindf  31514  nfesum1  31531  esumc  31542  esumrnmpt2  31559  esumsup  31580  esumgect  31581  esum2d  31584  sigapildsys  31653  ldgenpisyslem1  31654  voliune  31720  oms0  31787  rrvadd  31942  ballotlem7  32025  breprexplema  32133  cvmcov  32745  trpredlem1  33317  trpredrec  33328  rdgssun  35101  exrecfnlem  35102  phpreu  35347  matunitlindflem2  35360  poimirlem16  35379  poimirlem19  35382  itg2addnclem  35414  ftc1anclem5  35440  totbndbnd  35533  pwsgprod  39804  mzpsubmpt  40085  eq0rabdioph  40118  eqrabdioph  40119  aomclem8  40406  binomcxplemdvbinom  41458  binomcxplemdvsum  41460  binomcxplemnotnn0  41461  refsumcn  42060  refsum2cnlem1  42067  suprnmpt  42197  disjrnmpt2  42213  disjf1o  42216  fompt  42217  disjinfi  42218  choicefi  42227  axccdom  42249  rnmptbd2lem  42282  infnsuprnmpt  42284  rnmptbdlem  42289  rnmptss2  42291  rnmptssbi  42295  supxrleubrnmpt  42437  suprleubrnmpt  42453  infrnmptle  42454  infxrunb3rnmpt  42459  uzub  42462  supminfrnmpt  42476  infxrgelbrnmpt  42487  infrpgernmpt  42498  supminfxrrnmpt  42504  fmuldfeqlem1  42618  fmuldfeq  42619  climneg  42646  climdivf  42648  mullimc  42652  idlimc  42662  sumnnodd  42666  neglimc  42683  addlimc  42684  0ellimcdiv  42685  fnlimfvre  42710  fnlimabslt  42715  climreclmpt  42720  climfveqmpt2  42729  climeldmeqmpt2  42731  climeqmpt  42733  limsupubuz  42749  climinfmpt  42751  limsupubuzmpt  42755  limsupequzmptlem  42764  limsupre2mpt  42766  limsupre3mpt  42770  limsupreuzmpt  42775  liminflelimsuplem  42811  liminfvalxr  42819  liminfvalxrmpt  42822  liminfltlem  42840  liminflbuz2  42851  liminfpnfuz  42852  xlimmnfmpt  42879  xlimpnfmpt  42880  xlimpnfxnegmnf2  42894  cncfmptssg  42907  cncfshift  42910  cncficcgt0  42924  cncfiooicclem1  42929  dvnmul  42979  dvmptfprod  42981  itgsin0pilem1  42986  ibliccsinexp  42987  itgsinexplem1  42990  itgsinexp  42991  iblspltprt  43009  itgsubsticclem  43011  stoweidlem16  43052  stoweidlem18  43054  stoweidlem19  43055  stoweidlem20  43056  stoweidlem22  43058  stoweidlem23  43059  stoweidlem27  43063  stoweidlem31  43067  stoweidlem32  43068  stoweidlem34  43070  stoweidlem35  43071  stoweidlem36  43072  stoweidlem40  43076  stoweidlem41  43077  stoweidlem42  43078  stoweidlem43  43079  stoweidlem44  43080  stoweidlem45  43081  stoweidlem48  43084  stoweidlem51  43087  stoweidlem55  43091  stoweidlem59  43095  stoweidlem60  43096  stoweidlem62  43098  wallispilem5  43105  stirlinglem4  43113  stirlinglem5  43114  stirlinglem8  43117  stirlinglem11  43120  stirlinglem12  43121  stirlinglem13  43122  stirlinglem14  43123  stirlinglem15  43124  stirling  43125  fourierdlem16  43159  fourierdlem21  43164  fourierdlem22  43165  fourierdlem53  43195  fourierdlem68  43210  fourierdlem73  43215  fourierdlem80  43222  fourierdlem89  43231  fourierdlem91  43233  fourierdlem93  43235  fourierdlem103  43245  fourierdlem104  43246  fourierdlem112  43254  fourierdlem115  43257  fourierd  43258  fourierclimd  43259  etransclem48  43318  sge00  43409  sge0revalmpt  43411  sge0f1o  43415  sge0fsummpt  43423  sge0gerp  43428  sge0pnffigt  43429  sge0lefi  43431  sge0ltfirp  43433  sge0resplit  43439  sge0iunmptlemfi  43446  sge0iunmpt  43451  sge0xadd  43468  sge0fsummptf  43469  sge0gtfsumgt  43476  sge0reuz  43480  iundjiun  43493  meaiuninc3v  43517  omeiunltfirp  43552  omeiunlempt  43553  hoicvrrex  43589  ovncvrrp  43597  ovnhoilem1  43634  ovnlecvr2  43643  opnvonmbllem1  43665  iunhoiioolem  43708  pimgtmnf  43751  smfpimltmpt  43774  issmfdmpt  43776  smfconst  43777  smfpimltxrmpt  43786  smflimlem2  43799  smflim  43804  smfpimgtmpt  43808  smfpimgtxrmpt  43811  smfpimcclem  43832  smfpimcc  43833  smflimmpt  43835  smfsupmpt  43840  smfsupxr  43841  smfinfmpt  43844  smflimsuplem2  43846  smflimsuplem7  43851  smflimsupmpt  43854  smfliminfmpt  43857  1arymaptfo  45450  2arymaptfo  45461  aacllem  45793