Theorem nfmpt1 5225

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Ⅎwnfc 2884  {copab 5186   ↦ cmpt 5206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-opab 5187  df-mpt 5207

This theorem is referenced by:  nffvmpt1  6892  fvmptss  7003  fvmptd3f  7006  mpteqb  7010  fvmptf  7012  ralrnmptw  7089  ralrnmpt  7091  f1ompt  7106  fompt  7113  f1mpt  7259  fliftfun  7310  rdgsucmptf  8447  rdgsucmptnf  8448  frsucmpt  8457  frsucmptn  8458  dom2lem  9011  mapxpen  9162  cnfcom3clem  9724  ttrclselem1  9744  ttrclselem2  9745  infxpenc2lem2  10039  dfac8clem  10051  acnlem  10067  fin23lem32  10363  axcc3  10457  ac6num  10498  nfcprod1  15929  yonedalem4b  18293  prdsgsum  19967  cayleyhamilton1  22835  neiptopreu  23076  2ndcdisj  23399  ptcnp  23565  cnmpt11  23606  cnmptk2  23629  xkocnv  23757  utopsnneiplem  24191  restmetu  24514  mbfposr  25610  mbfsup  25622  itg1climres  25672  itg2splitlem  25706  itg2split  25707  itg2cnlem1  25719  nfitg1  25732  dvlipcn  25956  lhop2  25977  dvfsumabs  25986  itgparts  26011  itgsubstlem  26012  itgulm2  26375  lgamgulm2  27003  lgseisenlem2  27344  istrkg2ld  28444  cnlnadjlem5  32057  acunirnmpt2  32643  acunirnmpt2f  32644  aciunf1lem  32645  ofpreima  32648  fnpreimac  32654  disjdsct  32685  fpwrelmap  32715  prodindf  32845  elrgspnsubrunlem2  33248  nsgqusf1olem1  33433  nsgqusf1olem3  33435  elrspunidl  33448  fedgmullem2  33675  locfinreflem  33876  nfesum1  34076  esumc  34087  esumrnmpt2  34104  esumsup  34125  esumgect  34126  esum2d  34129  sigapildsys  34198  ldgenpisyslem1  34199  voliune  34265  oms0  34334  rrvadd  34489  ballotlem7  34573  breprexplema  34667  cvmcov  35290  rdgssun  37401  exrecfnlem  37402  phpreu  37633  matunitlindflem2  37646  poimirlem16  37665  poimirlem19  37668  itg2addnclem  37700  ftc1anclem5  37726  totbndbnd  37818  pwsgprod  42542  mzpsubmpt  42741  eq0rabdioph  42774  eqrabdioph  42775  aomclem8  43060  binomcxplemdvbinom  44352  binomcxplemdvsum  44354  binomcxplemnotnn0  44355  refsumcn  45034  refsum2cnlem1  45041  disjrnmpt2  45192  disjf1o  45195  disjinfi  45196  choicefi  45204  axccdom  45226  rnmptbd2lem  45252  infnsuprnmpt  45254  rnmptbdlem  45259  rnmptss2  45261  rnmptssbi  45264  supxrleubrnmpt  45413  suprleubrnmpt  45429  infrnmptle  45430  infxrunb3rnmpt  45435  uzub  45438  supminfrnmpt  45452  infxrgelbrnmpt  45461  infrpgernmpt  45472  supminfxrrnmpt  45478  fmuldfeqlem1  45591  fmuldfeq  45592  climneg  45619  climdivf  45621  mullimc  45625  idlimc  45635  sumnnodd  45639  neglimc  45656  addlimc  45657  0ellimcdiv  45658  fnlimfvre  45683  fnlimabslt  45688  climreclmpt  45693  climfveqmpt2  45702  climeldmeqmpt2  45704  climeqmpt  45706  limsupubuz  45722  climinfmpt  45724  limsupubuzmpt  45728  limsupequzmptlem  45737  limsupre2mpt  45739  limsupre3mpt  45743  limsupreuzmpt  45748  liminflelimsuplem  45784  liminfvalxr  45792  liminfvalxrmpt  45795  liminfltlem  45813  liminflbuz2  45824  liminfpnfuz  45825  xlimmnfmpt  45852  xlimpnfmpt  45853  xlimpnfxnegmnf2  45867  cncfmptssg  45880  cncfshift  45883  cncficcgt0  45897  cncfiooicclem1  45902  dvnmul  45952  dvmptfprod  45954  itgsin0pilem1  45959  ibliccsinexp  45960  itgsinexplem1  45963  itgsinexp  45964  iblspltprt  45982  itgsubsticclem  45984  stoweidlem16  46025  stoweidlem18  46027  stoweidlem19  46028  stoweidlem20  46029  stoweidlem22  46031  stoweidlem23  46032  stoweidlem27  46036  stoweidlem31  46040  stoweidlem32  46041  stoweidlem34  46043  stoweidlem35  46044  stoweidlem36  46045  stoweidlem40  46049  stoweidlem41  46050  stoweidlem42  46051  stoweidlem43  46052  stoweidlem44  46053  stoweidlem45  46054  stoweidlem48  46057  stoweidlem51  46060  stoweidlem55  46064  stoweidlem59  46068  stoweidlem60  46069  stoweidlem62  46071  wallispilem5  46078  stirlinglem4  46086  stirlinglem5  46087  stirlinglem8  46090  stirlinglem11  46093  stirlinglem12  46094  stirlinglem13  46095  stirlinglem14  46096  stirlinglem15  46097  stirling  46098  fourierdlem16  46132  fourierdlem21  46137  fourierdlem22  46138  fourierdlem68  46183  fourierdlem73  46188  fourierdlem80  46195  fourierdlem89  46204  fourierdlem91  46206  fourierdlem93  46208  fourierdlem103  46218  fourierdlem104  46219  fourierdlem112  46227  fourierdlem115  46230  fourierd  46231  fourierclimd  46232  etransclem48  46291  sge00  46385  sge0revalmpt  46387  sge0f1o  46391  sge0fsummpt  46399  sge0gerp  46404  sge0pnffigt  46405  sge0lefi  46407  sge0ltfirp  46409  sge0resplit  46415  sge0iunmptlemfi  46422  sge0iunmpt  46427  sge0xadd  46444  sge0fsummptf  46445  sge0gtfsumgt  46452  sge0reuz  46456  iundjiun  46469  meaiuninc3v  46493  omeiunltfirp  46528  omeiunlempt  46529  hoicvrrex  46565  ovncvrrp  46573  ovnhoilem1  46610  ovnlecvr2  46619  opnvonmbllem1  46641  iunhoiioolem  46684  smfpimltmpt  46755  issmfdmpt  46757  smfconst  46758  smfpimltxrmptf  46767  smflimlem2  46781  smflim  46786  smfpimgtmpt  46790  smfpimgtxrmptf  46793  smfpimcclem  46816  smfpimcc  46817  smflimmpt  46819  smfsupmpt  46824  smfsupxr  46825  smfinfmpt  46828  smflimsuplem2  46830  smflimsuplem7  46835  smflimsupmpt  46838  smfliminfmpt  46841  cfsetsnfsetf  47067  1arymaptfo  48603  2arymaptfo  48614  setrec2mpt  49541  aacllem  49645