Theorem nfmpt1 5212

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Ⅎwnfc 2912  {copab 5175   ↦ cmpt 5194

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-opab 5176  df-mpt 5195

This theorem is used by:  nffvmpt1  6896  fvmptss  7006  fvmptd3f  7009  mpteqb  7013  fvmptf  7015  ralrnmptw  7093  ralrnmpt  7095  f1ompt  7110  fompt  7117  f1mpt  7264  fliftfun  7319  rdgsucmptf  8421  rdgsucmptnf  8422  frsucmpt  8431  frsucmptn  8432  dom2lem  8995  mapxpen  9138  cnfcom3clem  9681  ttrclselem1  9701  ttrclselem2  9702  infxpenc2lem2  10020  dfac8clem  10032  acnlem  10048  fin23lem32  10343  axcc3  10437  ac6num  10478  nfcprod1  15985  yonedalem4b  18354  prdsgsum  20095  pwsgprod  20457  cayleyhamilton1  23099  neiptopreu  23340  2ndcdisj  23664  ptcnp  23830  cnmpt11  23871  cnmptk2  23894  xkocnv  24022  utopsnneiplem  24455  restmetu  24778  mbfposr  25862  mbfsup  25874  itg1climres  25924  itg2splitlem  25958  itg2split  25959  itg2cnlem1  25971  nfitg1  25984  dvlipcn  26204  lhop2  26225  dvfsumabs  26233  itgparts  26257  itgsubstlem  26258  itgulm2  26623  lgamgulm2  27251  lgseisenlem2  27591  istrkg2ld  28780  cnlnadjlem5  32494  acunirnmpt2  33076  acunirnmpt2f  33077  aciunf1lem  33078  ofpreima  33081  fnpreimac  33086  disjdsct  33119  fpwrelmap  33148  prodindf  33252  suppgsumssiun  33456  elrgspnsubrunlem2  33632  nsgqusf1olem1  33786  nsgqusf1olem3  33788  elrspunidl  33800  deg1prod  33937  mplvrpmga  33999  esplyfval1  34027  fedgmullem2  34084  locfinreflem  34294  nfesum1  34494  esumc  34505  esumrnmpt2  34522  esumsup  34543  esumgect  34544  esum2d  34547  sigapildsys  34617  ldgenpisyslem1  34618  voliune  34684  oms0  34752  rrvadd  34907  ballotlem7  34991  breprexplema  35082  cvmcov  35792  rdgssun  38081  exrecfnlem  38082  phpreu  38312  matunitlindflem2  38325  poimirlem16  38344  poimirlem19  38347  itg2addnclem  38379  ftc1anclem5  38405  totbndbnd  38498  mzpsubmpt  43532  eq0rabdioph  43565  eqrabdioph  43566  aomclem8  43846  binomcxplemdvbinom  45121  binomcxplemdvsum  45123  binomcxplemnotnn0  45124  refsumcn  45808  refsum2cnlem1  45815  disjrnmpt2  45964  disjf1o  45967  disjinfi  45968  choicefi  45975  axccdom  45996  rnmptbd2lem  46021  infnsuprnmpt  46023  rnmptbdlem  46028  rnmptss2  46030  rnmptssbi  46033  supxrleubrnmpt  46178  suprleubrnmpt  46194  infrnmptle  46195  infxrunb3rnmpt  46200  uzub  46203  supminfrnmpt  46217  infxrgelbrnmpt  46226  infrpgernmpt  46237  supminfxrrnmpt  46243  fmuldfeqlem1  46356  fmuldfeq  46357  climneg  46384  climdivf  46386  mullimc  46390  idlimc  46400  sumnnodd  46404  neglimc  46419  addlimc  46420  0ellimcdiv  46421  fnlimfvre  46446  fnlimabslt  46451  climreclmpt  46456  climfveqmpt2  46465  climeldmeqmpt2  46467  climeqmpt  46469  limsupubuz  46485  climinfmpt  46487  limsupubuzmpt  46491  limsupequzmptlem  46500  limsupre2mpt  46502  limsupre3mpt  46506  limsupreuzmpt  46511  liminflelimsuplem  46547  liminfvalxr  46555  liminfvalxrmpt  46558  liminfltlem  46576  liminflbuz2  46587  liminfpnfuz  46588  xlimmnfmpt  46615  xlimpnfmpt  46616  xlimpnfxnegmnf2  46630  cncfmptssg  46643  cncfshift  46646  cncficcgt0  46660  cncfiooicclem1  46665  dvnmul  46715  dvmptfprod  46717  itgsin0pilem1  46722  ibliccsinexp  46723  itgsinexplem1  46726  itgsinexp  46727  iblspltprt  46745  itgsubsticclem  46747  stoweidlem16  46788  stoweidlem18  46790  stoweidlem19  46791  stoweidlem20  46792  stoweidlem22  46794  stoweidlem23  46795  stoweidlem27  46799  stoweidlem31  46803  stoweidlem32  46804  stoweidlem34  46806  stoweidlem35  46807  stoweidlem36  46808  stoweidlem40  46812  stoweidlem41  46813  stoweidlem42  46814  stoweidlem43  46815  stoweidlem44  46816  stoweidlem45  46817  stoweidlem48  46820  stoweidlem51  46823  stoweidlem55  46827  stoweidlem59  46831  stoweidlem60  46832  stoweidlem62  46834  wallispilem5  46841  stirlinglem4  46849  stirlinglem5  46850  stirlinglem8  46853  stirlinglem11  46856  stirlinglem12  46857  stirlinglem13  46858  stirlinglem14  46859  stirlinglem15  46860  stirling  46861  fourierdlem16  46895  fourierdlem21  46900  fourierdlem22  46901  fourierdlem68  46946  fourierdlem73  46951  fourierdlem80  46958  fourierdlem89  46967  fourierdlem91  46969  fourierdlem93  46971  fourierdlem103  46981  fourierdlem104  46982  fourierdlem112  46990  fourierdlem115  46993  fourierd  46994  fourierclimd  46995  etransclem48  47054  sge00  47148  sge0revalmpt  47150  sge0f1o  47154  sge0fsummpt  47162  sge0gerp  47167  sge0pnffigt  47168  sge0lefi  47170  sge0ltfirp  47172  sge0resplit  47178  sge0iunmptlemfi  47185  sge0iunmpt  47190  sge0xadd  47207  sge0fsummptf  47208  sge0gtfsumgt  47215  sge0reuz  47219  iundjiun  47232  meaiuninc3v  47256  omeiunltfirp  47291  omeiunlempt  47292  hoicvrrex  47328  ovncvrrp  47336  ovnhoilem1  47373  ovnlecvr2  47382  opnvonmbllem1  47404  iunhoiioolem  47447  smfpimltmpt  47518  issmfdmpt  47520  smfconst  47521  smfpimltxrmptf  47530  smflimlem2  47544  smflim  47549  smfpimgtmpt  47553  smfpimgtxrmptf  47556  smfpimcclem  47579  smfpimcc  47580  smflimmpt  47582  smfsupmpt  47587  smfsupxr  47588  smfinfmpt  47591  smflimsuplem2  47593  smflimsuplem7  47598  smflimsupmpt  47601  smfliminfmpt  47604  cfsetsnfsetf  47853  1arymaptfo  49480  2arymaptfo  49491  setrec2mpt  50532  aacllem  50678