Theorem nfmpt1 5210

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Ⅎwnfc 2911  {copab 5173   ↦ cmpt 5192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-opab 5174  df-mpt 5193

This theorem is used by:  nffvmpt1  6927  fvmptss  7037  fvmptd3f  7040  mpteqb  7044  fvmptf  7046  ralrnmptw  7126  ralrnmpt  7128  f1ompt  7143  fompt  7150  f1mpt  7296  fliftfun  7351  rdgsucmptf  8474  rdgsucmptnf  8475  frsucmpt  8484  frsucmptn  8485  dom2lem  9057  mapxpen  9200  cnfcom3clem  9743  ttrclselem1  9763  ttrclselem2  9764  infxpenc2lem2  10138  dfac8clem  10150  acnlem  10166  fin23lem32  10461  axcc3  10555  ac6num  10596  nfcprod1  16121  yonedalem4b  18500  prdsgsum  20246  pwsgprod  20610  matunitlindflem2  23050  cayleyhamilton1  23265  neiptopreu  23506  2ndcdisj  23830  ptcnp  23996  cnmpt11  24037  cnmptk2  24060  xkocnv  24188  utopsnneiplem  24621  restmetu  24944  mbfposr  26028  mbfsup  26040  itg1climres  26090  itg2splitlem  26124  itg2split  26125  itg2cnlem1  26137  nfitg1  26149  dvlipcn  26369  lhop2  26390  dvfsumabs  26398  itgparts  26422  itgsubstlem  26423  itgulm2  26793  lgamgulm2  27420  lgseisenlem2  27760  istrkg2ld  28979  cnlnadjlem5  32730  acunirnmpt2  33352  acunirnmpt2f  33353  aciunf1lem  33354  ofpreima  33357  fnpreimac  33362  disjdsct  33393  fpwrelmap  33421  prodindf  33525  suppgsumssiun  33732  elrgspnsubrunlem2  33908  nsgqusf1olem1  34068  nsgqusf1olem3  34070  elrspunidl  34082  deg1prod  34218  mplvrpmga  34288  esplyfval1  34316  fedgmullem2  34373  locfinreflem  34583  nfesum1  34783  esumc  34794  esumrnmpt2  34811  esumsup  34832  esumgect  34833  esum2d  34836  sigapildsys  34906  ldgenpisyslem1  34907  voliune  34973  oms0  35040  rrvadd  35195  ballotlem7  35279  breprexplema  35370  cvmcov  36236  rdgssun  38569  exrecfnlem  38570  phpreu  38795  poimirlem16  38822  poimirlem19  38825  itg2addnclem  38857  ftc1anclem5  38883  totbndbnd  38989  mzpsubmpt  44020  eq0rabdioph  44053  eqrabdioph  44054  aomclem8  44329  binomcxplemdvbinom  45598  binomcxplemdvsum  45600  binomcxplemnotnn0  45601  refsumcn  46321  refsum2cnlem1  46328  disjrnmpt2  46476  disjf1o  46479  disjinfi  46480  choicefi  46487  axccdom  46508  rnmptbd2lem  46533  infnsuprnmpt  46535  rnmptbdlem  46540  rnmptss2  46542  rnmptssbi  46545  supxrleubrnmpt  46689  suprleubrnmpt  46705  infrnmptle  46706  infxrunb3rnmpt  46711  uzub  46714  supminfrnmpt  46728  infxrgelbrnmpt  46737  infrpgernmpt  46748  supminfxrrnmpt  46754  fmuldfeqlem1  46867  fmuldfeq  46868  climneg  46895  climdivf  46897  mullimc  46901  idlimc  46911  sumnnodd  46915  neglimc  46930  addlimc  46931  0ellimcdiv  46932  fnlimfvre  46957  fnlimabslt  46962  climreclmpt  46967  climfveqmpt2  46976  climeldmeqmpt2  46978  climeqmpt  46980  limsupubuz  46996  climinfmpt  46998  limsupubuzmpt  47002  limsupequzmptlem  47011  limsupre2mpt  47013  limsupre3mpt  47017  limsupreuzmpt  47022  liminflelimsuplem  47058  liminfvalxr  47066  liminfvalxrmpt  47069  liminfltlem  47087  liminflbuz2  47098  liminfpnfuz  47099  xlimmnfmpt  47126  xlimpnfmpt  47127  xlimpnfxnegmnf2  47141  cncfmptssg  47154  cncfshift  47157  cncficcgt0  47171  cncfiooicclem1  47176  dvnmul  47226  dvmptfprod  47228  itgsin0pilem1  47233  ibliccsinexp  47234  itgsinexplem1  47237  itgsinexp  47238  iblspltprt  47256  itgsubsticclem  47258  stoweidlem16  47299  stoweidlem18  47301  stoweidlem19  47302  stoweidlem20  47303  stoweidlem22  47305  stoweidlem23  47306  stoweidlem27  47310  stoweidlem31  47314  stoweidlem32  47315  stoweidlem34  47317  stoweidlem35  47318  stoweidlem36  47319  stoweidlem40  47323  stoweidlem41  47324  stoweidlem42  47325  stoweidlem43  47326  stoweidlem44  47327  stoweidlem45  47328  stoweidlem48  47331  stoweidlem51  47334  stoweidlem55  47338  stoweidlem59  47342  stoweidlem60  47343  stoweidlem62  47345  wallispilem5  47352  stirlinglem4  47360  stirlinglem5  47361  stirlinglem8  47364  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  stirling  47372  fourierdlem16  47406  fourierdlem21  47411  fourierdlem22  47412  fourierdlem68  47457  fourierdlem73  47462  fourierdlem80  47469  fourierdlem89  47478  fourierdlem91  47480  fourierdlem93  47482  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  fourierdlem115  47504  fourierd  47505  fourierclimd  47506  etransclem48  47565  sge00  47659  sge0revalmpt  47661  sge0f1o  47665  sge0fsummpt  47673  sge0gerp  47678  sge0pnffigt  47679  sge0lefi  47681  sge0ltfirp  47683  sge0resplit  47689  sge0iunmptlemfi  47696  sge0iunmpt  47701  sge0xadd  47718  sge0fsummptf  47719  sge0gtfsumgt  47726  sge0reuz  47730  iundjiun  47743  meaiuninc3v  47767  omeiunltfirp  47802  omeiunlempt  47803  hoicvrrex  47839  ovncvrrp  47847  ovnhoilem1  47884  ovnlecvr2  47893  opnvonmbllem1  47915  iunhoiioolem  47958  smfpimltmpt  48029  issmfdmpt  48031  smfconst  48032  smfpimltxrmptf  48041  smflimlem2  48055  smflim  48060  smfpimgtmpt  48064  smfpimgtxrmptf  48067  smfpimcclem  48090  smfpimcc  48091  smflimmpt  48093  smfsupmpt  48098  smfsupxr  48099  smfinfmpt  48102  smflimsuplem2  48104  smflimsuplem7  48109  smflimsupmpt  48112  smfliminfmpt  48115  cfsetsnfsetf  48401  1arymaptfo  50086  2arymaptfo  50097  setrec2mpt  51196  aacllem  51367