Theorem nfmpt1 5249

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

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Ⅎwnfc 2889  {copab 5204   ↦ cmpt 5224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-opab 5205  df-mpt 5225

This theorem is referenced by:  nffvmpt1  6916  fvmptss  7027  fvmptd3f  7030  mpteqb  7034  fvmptf  7036  ralrnmptw  7113  ralrnmpt  7115  f1ompt  7130  fompt  7137  f1mpt  7282  fliftfun  7333  rdgsucmptf  8469  rdgsucmptnf  8470  frsucmpt  8479  frsucmptn  8480  dom2lem  9033  mapxpen  9184  cnfcom3clem  9746  ttrclselem1  9766  ttrclselem2  9767  infxpenc2lem2  10061  dfac8clem  10073  acnlem  10089  fin23lem32  10385  axcc3  10479  ac6num  10520  nfcprod1  15945  yonedalem4b  18322  prdsgsum  20000  cayleyhamilton1  22899  neiptopreu  23142  2ndcdisj  23465  ptcnp  23631  cnmpt11  23672  cnmptk2  23695  xkocnv  23823  utopsnneiplem  24257  restmetu  24584  mbfposr  25688  mbfsup  25700  itg1climres  25750  itg2splitlem  25784  itg2split  25785  itg2cnlem1  25797  nfitg1  25810  dvlipcn  26034  lhop2  26055  dvfsumabs  26064  itgparts  26089  itgsubstlem  26090  itgulm2  26453  lgamgulm2  27080  lgseisenlem2  27421  istrkg2ld  28469  cnlnadjlem5  32091  acunirnmpt2  32671  acunirnmpt2f  32672  aciunf1lem  32673  ofpreima  32676  fnpreimac  32682  disjdsct  32713  fpwrelmap  32745  prodindf  32849  elrgspnsubrunlem2  33253  nsgqusf1olem1  33442  nsgqusf1olem3  33444  elrspunidl  33457  fedgmullem2  33682  locfinreflem  33840  nfesum1  34042  esumc  34053  esumrnmpt2  34070  esumsup  34091  esumgect  34092  esum2d  34095  sigapildsys  34164  ldgenpisyslem1  34165  voliune  34231  oms0  34300  rrvadd  34455  ballotlem7  34539  breprexplema  34646  cvmcov  35269  rdgssun  37380  exrecfnlem  37381  phpreu  37612  matunitlindflem2  37625  poimirlem16  37644  poimirlem19  37647  itg2addnclem  37679  ftc1anclem5  37705  totbndbnd  37797  pwsgprod  42559  mzpsubmpt  42759  eq0rabdioph  42792  eqrabdioph  42793  aomclem8  43078  binomcxplemdvbinom  44377  binomcxplemdvsum  44379  binomcxplemnotnn0  44380  refsumcn  45040  refsum2cnlem1  45047  disjrnmpt2  45198  disjf1o  45201  disjinfi  45202  choicefi  45210  axccdom  45232  rnmptbd2lem  45260  infnsuprnmpt  45262  rnmptbdlem  45267  rnmptss2  45269  rnmptssbi  45272  supxrleubrnmpt  45422  suprleubrnmpt  45438  infrnmptle  45439  infxrunb3rnmpt  45444  uzub  45447  supminfrnmpt  45461  infxrgelbrnmpt  45470  infrpgernmpt  45481  supminfxrrnmpt  45487  fmuldfeqlem1  45602  fmuldfeq  45603  climneg  45630  climdivf  45632  mullimc  45636  idlimc  45646  sumnnodd  45650  neglimc  45667  addlimc  45668  0ellimcdiv  45669  fnlimfvre  45694  fnlimabslt  45699  climreclmpt  45704  climfveqmpt2  45713  climeldmeqmpt2  45715  climeqmpt  45717  limsupubuz  45733  climinfmpt  45735  limsupubuzmpt  45739  limsupequzmptlem  45748  limsupre2mpt  45750  limsupre3mpt  45754  limsupreuzmpt  45759  liminflelimsuplem  45795  liminfvalxr  45803  liminfvalxrmpt  45806  liminfltlem  45824  liminflbuz2  45835  liminfpnfuz  45836  xlimmnfmpt  45863  xlimpnfmpt  45864  xlimpnfxnegmnf2  45878  cncfmptssg  45891  cncfshift  45894  cncficcgt0  45908  cncfiooicclem1  45913  dvnmul  45963  dvmptfprod  45965  itgsin0pilem1  45970  ibliccsinexp  45971  itgsinexplem1  45974  itgsinexp  45975  iblspltprt  45993  itgsubsticclem  45995  stoweidlem16  46036  stoweidlem18  46038  stoweidlem19  46039  stoweidlem20  46040  stoweidlem22  46042  stoweidlem23  46043  stoweidlem27  46047  stoweidlem31  46051  stoweidlem32  46052  stoweidlem34  46054  stoweidlem35  46055  stoweidlem36  46056  stoweidlem40  46060  stoweidlem41  46061  stoweidlem42  46062  stoweidlem43  46063  stoweidlem44  46064  stoweidlem45  46065  stoweidlem48  46068  stoweidlem51  46071  stoweidlem55  46075  stoweidlem59  46079  stoweidlem60  46080  stoweidlem62  46082  wallispilem5  46089  stirlinglem4  46097  stirlinglem5  46098  stirlinglem8  46101  stirlinglem11  46104  stirlinglem12  46105  stirlinglem13  46106  stirlinglem14  46107  stirlinglem15  46108  stirling  46109  fourierdlem16  46143  fourierdlem21  46148  fourierdlem22  46149  fourierdlem68  46194  fourierdlem73  46199  fourierdlem80  46206  fourierdlem89  46215  fourierdlem91  46217  fourierdlem93  46219  fourierdlem103  46229  fourierdlem104  46230  fourierdlem112  46238  fourierdlem115  46241  fourierd  46242  fourierclimd  46243  etransclem48  46302  sge00  46396  sge0revalmpt  46398  sge0f1o  46402  sge0fsummpt  46410  sge0gerp  46415  sge0pnffigt  46416  sge0lefi  46418  sge0ltfirp  46420  sge0resplit  46426  sge0iunmptlemfi  46433  sge0iunmpt  46438  sge0xadd  46455  sge0fsummptf  46456  sge0gtfsumgt  46463  sge0reuz  46467  iundjiun  46480  meaiuninc3v  46504  omeiunltfirp  46539  omeiunlempt  46540  hoicvrrex  46576  ovncvrrp  46584  ovnhoilem1  46621  ovnlecvr2  46630  opnvonmbllem1  46652  iunhoiioolem  46695  smfpimltmpt  46766  issmfdmpt  46768  smfconst  46769  smfpimltxrmptf  46778  smflimlem2  46792  smflim  46797  smfpimgtmpt  46801  smfpimgtxrmptf  46804  smfpimcclem  46827  smfpimcc  46828  smflimmpt  46830  smfsupmpt  46835  smfsupxr  46836  smfinfmpt  46839  smflimsuplem2  46841  smflimsuplem7  46846  smflimsupmpt  46849  smfliminfmpt  46852  cfsetsnfsetf  47075  1arymaptfo  48569  2arymaptfo  48580  setrec2mpt  49271  aacllem  49375