Theorem nfmpt1 5183

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

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2107  Ⅎwnfc 2888  {copab 5137   ↦ cmpt 5158

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-opab 5138  df-mpt 5159

This theorem is referenced by:  nffvmpt1  6794  fvmptss  6896  fvmptd3f  6899  mpteqb  6903  fvmptf  6905  ralrnmptw  6979  ralrnmpt  6981  f1ompt  6994  f1mpt  7143  fliftfun  7192  rdgsucmptf  8268  rdgsucmptnf  8269  frsucmpt  8278  frsucmptn  8279  dom2lem  8789  mapxpen  8939  cnfcom3clem  9472  ttrclselem1  9492  ttrclselem2  9493  infxpenc2lem2  9785  dfac8clem  9797  acnlem  9813  fin23lem32  10109  axcc3  10203  ac6num  10244  nfcprod1  15629  yonedalem4b  18003  prdsgsum  19591  cayleyhamilton1  22050  neiptopreu  22293  2ndcdisj  22616  ptcnp  22782  cnmpt11  22823  cnmptk2  22846  xkocnv  22974  utopsnneiplem  23408  restmetu  23735  mbfposr  24825  mbfsup  24837  itg1climres  24888  itg2splitlem  24922  itg2split  24923  itg2cnlem1  24935  nfitg1  24947  dvlipcn  25167  lhop2  25188  dvfsumabs  25196  itgparts  25220  itgsubstlem  25221  itgulm2  25577  lgamgulm2  26194  lgseisenlem2  26533  istrkg2ld  26830  cnlnadjlem5  30442  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1lem  31008  ofpreima  31011  fnpreimac  31017  disjdsct  31044  fpwrelmap  31077  nsgqusf1olem1  31607  nsgqusf1olem3  31609  elrspunidl  31615  fedgmullem2  31720  locfinreflem  31799  prodindf  32000  nfesum1  32017  esumc  32028  esumrnmpt2  32045  esumsup  32066  esumgect  32067  esum2d  32070  sigapildsys  32139  ldgenpisyslem1  32140  voliune  32206  oms0  32273  rrvadd  32428  ballotlem7  32511  breprexplema  32619  cvmcov  33234  rdgssun  35558  exrecfnlem  35559  phpreu  35770  matunitlindflem2  35783  poimirlem16  35802  poimirlem19  35805  itg2addnclem  35837  ftc1anclem5  35863  totbndbnd  35956  pwsgprod  40276  mzpsubmpt  40572  eq0rabdioph  40605  eqrabdioph  40606  aomclem8  40893  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  refsumcn  42580  refsum2cnlem1  42587  disjrnmpt2  42733  disjf1o  42736  fompt  42737  disjinfi  42738  choicefi  42747  axccdom  42769  rnmptbd2lem  42801  infnsuprnmpt  42803  rnmptbdlem  42808  rnmptss2  42810  rnmptssbi  42814  supxrleubrnmpt  42953  suprleubrnmpt  42969  infrnmptle  42970  infxrunb3rnmpt  42975  uzub  42978  supminfrnmpt  42992  infxrgelbrnmpt  43001  infrpgernmpt  43012  supminfxrrnmpt  43018  fmuldfeqlem1  43130  fmuldfeq  43131  climneg  43158  climdivf  43160  mullimc  43164  idlimc  43174  sumnnodd  43178  neglimc  43195  addlimc  43196  0ellimcdiv  43197  fnlimfvre  43222  fnlimabslt  43227  climreclmpt  43232  climfveqmpt2  43241  climeldmeqmpt2  43243  climeqmpt  43245  limsupubuz  43261  climinfmpt  43263  limsupubuzmpt  43267  limsupequzmptlem  43276  limsupre2mpt  43278  limsupre3mpt  43282  limsupreuzmpt  43287  liminflelimsuplem  43323  liminfvalxr  43331  liminfvalxrmpt  43334  liminfltlem  43352  liminflbuz2  43363  liminfpnfuz  43364  xlimmnfmpt  43391  xlimpnfmpt  43392  xlimpnfxnegmnf2  43406  cncfmptssg  43419  cncfshift  43422  cncficcgt0  43436  cncfiooicclem1  43441  dvnmul  43491  dvmptfprod  43493  itgsin0pilem1  43498  ibliccsinexp  43499  itgsinexplem1  43502  itgsinexp  43503  iblspltprt  43521  itgsubsticclem  43523  stoweidlem16  43564  stoweidlem18  43566  stoweidlem19  43567  stoweidlem20  43568  stoweidlem22  43570  stoweidlem23  43571  stoweidlem27  43575  stoweidlem31  43579  stoweidlem32  43580  stoweidlem34  43582  stoweidlem35  43583  stoweidlem36  43584  stoweidlem40  43588  stoweidlem41  43589  stoweidlem42  43590  stoweidlem43  43591  stoweidlem44  43592  stoweidlem45  43593  stoweidlem48  43596  stoweidlem51  43599  stoweidlem55  43603  stoweidlem59  43607  stoweidlem60  43608  stoweidlem62  43610  wallispilem5  43617  stirlinglem4  43625  stirlinglem5  43626  stirlinglem8  43629  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  stirling  43637  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem68  43722  fourierdlem73  43727  fourierdlem80  43734  fourierdlem89  43743  fourierdlem91  43745  fourierdlem93  43747  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem115  43769  fourierd  43770  fourierclimd  43771  etransclem48  43830  sge00  43921  sge0revalmpt  43923  sge0f1o  43927  sge0fsummpt  43935  sge0gerp  43940  sge0pnffigt  43941  sge0lefi  43943  sge0ltfirp  43945  sge0resplit  43951  sge0iunmptlemfi  43958  sge0iunmpt  43963  sge0xadd  43980  sge0fsummptf  43981  sge0gtfsumgt  43988  sge0reuz  43992  iundjiun  44005  meaiuninc3v  44029  omeiunltfirp  44064  omeiunlempt  44065  hoicvrrex  44101  ovncvrrp  44109  ovnhoilem1  44146  ovnlecvr2  44155  opnvonmbllem1  44177  iunhoiioolem  44220  smfpimltmpt  44291  issmfdmpt  44293  smfconst  44294  smfpimltxrmptf  44303  smflimlem2  44317  smflim  44322  smfpimgtmpt  44326  smfpimgtxrmptf  44329  smfpimcclem  44351  smfpimcc  44352  smflimmpt  44354  smfsupmpt  44359  smfsupxr  44360  smfinfmpt  44363  smflimsuplem2  44365  smflimsuplem7  44370  smflimsupmpt  44373  smfliminfmpt  44376  cfsetsnfsetf  44563  1arymaptfo  46000  2arymaptfo  46011  aacllem  46516