Theorem nfmpt1 5257

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

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Ⅎwnfc 2884  {copab 5211   ↦ cmpt 5232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-opab 5212  df-mpt 5233

This theorem is referenced by:  nffvmpt1  6903  fvmptss  7011  fvmptd3f  7014  mpteqb  7018  fvmptf  7020  ralrnmptw  7096  ralrnmpt  7098  f1ompt  7111  f1mpt  7260  fliftfun  7309  rdgsucmptf  8428  rdgsucmptnf  8429  frsucmpt  8438  frsucmptn  8439  dom2lem  8988  mapxpen  9143  cnfcom3clem  9700  ttrclselem1  9720  ttrclselem2  9721  infxpenc2lem2  10015  dfac8clem  10027  acnlem  10043  fin23lem32  10339  axcc3  10433  ac6num  10474  nfcprod1  15854  yonedalem4b  18229  prdsgsum  19849  cayleyhamilton1  22394  neiptopreu  22637  2ndcdisj  22960  ptcnp  23126  cnmpt11  23167  cnmptk2  23190  xkocnv  23318  utopsnneiplem  23752  restmetu  24079  mbfposr  25169  mbfsup  25181  itg1climres  25232  itg2splitlem  25266  itg2split  25267  itg2cnlem1  25279  nfitg1  25291  dvlipcn  25511  lhop2  25532  dvfsumabs  25540  itgparts  25564  itgsubstlem  25565  itgulm2  25921  lgamgulm2  26540  lgseisenlem2  26879  istrkg2ld  27711  cnlnadjlem5  31324  acunirnmpt2  31885  acunirnmpt2f  31886  aciunf1lem  31887  ofpreima  31890  fnpreimac  31896  disjdsct  31924  fpwrelmap  31958  nsgqusf1olem1  32524  nsgqusf1olem3  32526  elrspunidl  32546  fedgmullem2  32715  locfinreflem  32820  prodindf  33021  nfesum1  33038  esumc  33049  esumrnmpt2  33066  esumsup  33087  esumgect  33088  esum2d  33091  sigapildsys  33160  ldgenpisyslem1  33161  voliune  33227  oms0  33296  rrvadd  33451  ballotlem7  33534  breprexplema  33642  cvmcov  34254  rdgssun  36259  exrecfnlem  36260  phpreu  36472  matunitlindflem2  36485  poimirlem16  36504  poimirlem19  36507  itg2addnclem  36539  ftc1anclem5  36565  totbndbnd  36657  pwsgprod  41114  mzpsubmpt  41481  eq0rabdioph  41514  eqrabdioph  41515  aomclem8  41803  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  refsumcn  43714  refsum2cnlem1  43721  disjrnmpt2  43886  disjf1o  43889  fompt  43890  disjinfi  43891  choicefi  43899  axccdom  43921  rnmptbd2lem  43952  infnsuprnmpt  43954  rnmptbdlem  43959  rnmptss2  43961  rnmptssbi  43965  supxrleubrnmpt  44116  suprleubrnmpt  44132  infrnmptle  44133  infxrunb3rnmpt  44138  uzub  44141  supminfrnmpt  44155  infxrgelbrnmpt  44164  infrpgernmpt  44175  supminfxrrnmpt  44181  fmuldfeqlem1  44298  fmuldfeq  44299  climneg  44326  climdivf  44328  mullimc  44332  idlimc  44342  sumnnodd  44346  neglimc  44363  addlimc  44364  0ellimcdiv  44365  fnlimfvre  44390  fnlimabslt  44395  climreclmpt  44400  climfveqmpt2  44409  climeldmeqmpt2  44411  climeqmpt  44413  limsupubuz  44429  climinfmpt  44431  limsupubuzmpt  44435  limsupequzmptlem  44444  limsupre2mpt  44446  limsupre3mpt  44450  limsupreuzmpt  44455  liminflelimsuplem  44491  liminfvalxr  44499  liminfvalxrmpt  44502  liminfltlem  44520  liminflbuz2  44531  liminfpnfuz  44532  xlimmnfmpt  44559  xlimpnfmpt  44560  xlimpnfxnegmnf2  44574  cncfmptssg  44587  cncfshift  44590  cncficcgt0  44604  cncfiooicclem1  44609  dvnmul  44659  dvmptfprod  44661  itgsin0pilem1  44666  ibliccsinexp  44667  itgsinexplem1  44670  itgsinexp  44671  iblspltprt  44689  itgsubsticclem  44691  stoweidlem16  44732  stoweidlem18  44734  stoweidlem19  44735  stoweidlem20  44736  stoweidlem22  44738  stoweidlem23  44739  stoweidlem27  44743  stoweidlem31  44747  stoweidlem32  44748  stoweidlem34  44750  stoweidlem35  44751  stoweidlem36  44752  stoweidlem40  44756  stoweidlem41  44757  stoweidlem42  44758  stoweidlem43  44759  stoweidlem44  44760  stoweidlem45  44761  stoweidlem48  44764  stoweidlem51  44767  stoweidlem55  44771  stoweidlem59  44775  stoweidlem60  44776  stoweidlem62  44778  wallispilem5  44785  stirlinglem4  44793  stirlinglem5  44794  stirlinglem8  44797  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  stirling  44805  fourierdlem16  44839  fourierdlem21  44844  fourierdlem22  44845  fourierdlem68  44890  fourierdlem73  44895  fourierdlem80  44902  fourierdlem89  44911  fourierdlem91  44913  fourierdlem93  44915  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  fourierdlem115  44937  fourierd  44938  fourierclimd  44939  etransclem48  44998  sge00  45092  sge0revalmpt  45094  sge0f1o  45098  sge0fsummpt  45106  sge0gerp  45111  sge0pnffigt  45112  sge0lefi  45114  sge0ltfirp  45116  sge0resplit  45122  sge0iunmptlemfi  45129  sge0iunmpt  45134  sge0xadd  45151  sge0fsummptf  45152  sge0gtfsumgt  45159  sge0reuz  45163  iundjiun  45176  meaiuninc3v  45200  omeiunltfirp  45235  omeiunlempt  45236  hoicvrrex  45272  ovncvrrp  45280  ovnhoilem1  45317  ovnlecvr2  45326  opnvonmbllem1  45348  iunhoiioolem  45391  smfpimltmpt  45462  issmfdmpt  45464  smfconst  45465  smfpimltxrmptf  45474  smflimlem2  45488  smflim  45493  smfpimgtmpt  45497  smfpimgtxrmptf  45500  smfpimcclem  45523  smfpimcc  45524  smflimmpt  45526  smfsupmpt  45531  smfsupxr  45532  smfinfmpt  45535  smflimsuplem2  45537  smflimsuplem7  45542  smflimsupmpt  45545  smfliminfmpt  45548  cfsetsnfsetf  45768  1arymaptfo  47329  2arymaptfo  47340  setrec2mpt  47742  aacllem  47848