Theorem nfmpt1 5204

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Ⅎwnfc 2907  {copab 5167   ↦ cmpt 5186

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-opab 5168  df-mpt 5187

This theorem is used by:  nffvmpt1  6889  fvmptss  6999  fvmptd3f  7002  mpteqb  7006  fvmptf  7008  ralrnmptw  7087  ralrnmpt  7089  f1ompt  7104  fompt  7111  f1mpt  7258  fliftfun  7313  rdgsucmptf  8417  rdgsucmptnf  8418  frsucmpt  8427  frsucmptn  8428  dom2lem  8998  mapxpen  9141  cnfcom3clem  9684  ttrclselem1  9704  ttrclselem2  9705  infxpenc2lem2  10023  dfac8clem  10035  acnlem  10051  fin23lem32  10346  axcc3  10440  ac6num  10481  nfcprod1  15997  yonedalem4b  18364  prdsgsum  20108  pwsgprod  20470  matunitlindflem2  22902  cayleyhamilton1  23117  neiptopreu  23358  2ndcdisj  23682  ptcnp  23848  cnmpt11  23889  cnmptk2  23912  xkocnv  24040  utopsnneiplem  24473  restmetu  24796  mbfposr  25880  mbfsup  25892  itg1climres  25942  itg2splitlem  25976  itg2split  25977  itg2cnlem1  25989  nfitg1  26001  dvlipcn  26221  lhop2  26242  dvfsumabs  26250  itgparts  26274  itgsubstlem  26275  itgulm2  26645  lgamgulm2  27272  lgseisenlem2  27612  istrkg2ld  28801  cnlnadjlem5  32552  acunirnmpt2  33133  acunirnmpt2f  33134  aciunf1lem  33135  ofpreima  33138  fnpreimac  33143  disjdsct  33175  fpwrelmap  33204  prodindf  33308  suppgsumssiun  33512  elrgspnsubrunlem2  33688  nsgqusf1olem1  33842  nsgqusf1olem3  33844  elrspunidl  33856  deg1prod  33993  mplvrpmga  34055  esplyfval1  34083  fedgmullem2  34140  locfinreflem  34350  nfesum1  34550  esumc  34561  esumrnmpt2  34578  esumsup  34599  esumgect  34600  esum2d  34603  sigapildsys  34673  ldgenpisyslem1  34674  voliune  34740  oms0  34808  rrvadd  34963  ballotlem7  35047  breprexplema  35138  cvmcov  35842  rdgssun  38132  exrecfnlem  38133  phpreu  38358  poimirlem16  38385  poimirlem19  38388  itg2addnclem  38420  ftc1anclem5  38446  totbndbnd  38539  mzpsubmpt  43588  eq0rabdioph  43621  eqrabdioph  43622  aomclem8  43902  binomcxplemdvbinom  45177  binomcxplemdvsum  45179  binomcxplemnotnn0  45180  refsumcn  45864  refsum2cnlem1  45871  disjrnmpt2  46020  disjf1o  46023  disjinfi  46024  choicefi  46031  axccdom  46052  rnmptbd2lem  46077  infnsuprnmpt  46079  rnmptbdlem  46084  rnmptss2  46086  rnmptssbi  46089  supxrleubrnmpt  46234  suprleubrnmpt  46250  infrnmptle  46251  infxrunb3rnmpt  46256  uzub  46259  supminfrnmpt  46273  infxrgelbrnmpt  46282  infrpgernmpt  46293  supminfxrrnmpt  46299  fmuldfeqlem1  46412  fmuldfeq  46413  climneg  46440  climdivf  46442  mullimc  46446  idlimc  46456  sumnnodd  46460  neglimc  46475  addlimc  46476  0ellimcdiv  46477  fnlimfvre  46502  fnlimabslt  46507  climreclmpt  46512  climfveqmpt2  46521  climeldmeqmpt2  46523  climeqmpt  46525  limsupubuz  46541  climinfmpt  46543  limsupubuzmpt  46547  limsupequzmptlem  46556  limsupre2mpt  46558  limsupre3mpt  46562  limsupreuzmpt  46567  liminflelimsuplem  46603  liminfvalxr  46611  liminfvalxrmpt  46614  liminfltlem  46632  liminflbuz2  46643  liminfpnfuz  46644  xlimmnfmpt  46671  xlimpnfmpt  46672  xlimpnfxnegmnf2  46686  cncfmptssg  46699  cncfshift  46702  cncficcgt0  46716  cncfiooicclem1  46721  dvnmul  46771  dvmptfprod  46773  itgsin0pilem1  46778  ibliccsinexp  46779  itgsinexplem1  46782  itgsinexp  46783  iblspltprt  46801  itgsubsticclem  46803  stoweidlem16  46844  stoweidlem18  46846  stoweidlem19  46847  stoweidlem20  46848  stoweidlem22  46850  stoweidlem23  46851  stoweidlem27  46855  stoweidlem31  46859  stoweidlem32  46860  stoweidlem34  46862  stoweidlem35  46863  stoweidlem36  46864  stoweidlem40  46868  stoweidlem41  46869  stoweidlem42  46870  stoweidlem43  46871  stoweidlem44  46872  stoweidlem45  46873  stoweidlem48  46876  stoweidlem51  46879  stoweidlem55  46883  stoweidlem59  46887  stoweidlem60  46888  stoweidlem62  46890  wallispilem5  46897  stirlinglem4  46905  stirlinglem5  46906  stirlinglem8  46909  stirlinglem11  46912  stirlinglem12  46913  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  stirling  46917  fourierdlem16  46951  fourierdlem21  46956  fourierdlem22  46957  fourierdlem68  47002  fourierdlem73  47007  fourierdlem80  47014  fourierdlem89  47023  fourierdlem91  47025  fourierdlem93  47027  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  fourierdlem115  47049  fourierd  47050  fourierclimd  47051  etransclem48  47110  sge00  47204  sge0revalmpt  47206  sge0f1o  47210  sge0fsummpt  47218  sge0gerp  47223  sge0pnffigt  47224  sge0lefi  47226  sge0ltfirp  47228  sge0resplit  47234  sge0iunmptlemfi  47241  sge0iunmpt  47246  sge0xadd  47263  sge0fsummptf  47264  sge0gtfsumgt  47271  sge0reuz  47275  iundjiun  47288  meaiuninc3v  47312  omeiunltfirp  47347  omeiunlempt  47348  hoicvrrex  47384  ovncvrrp  47392  ovnhoilem1  47429  ovnlecvr2  47438  opnvonmbllem1  47460  iunhoiioolem  47503  smfpimltmpt  47574  issmfdmpt  47576  smfconst  47577  smfpimltxrmptf  47586  smflimlem2  47600  smflim  47605  smfpimgtmpt  47609  smfpimgtxrmptf  47612  smfpimcclem  47635  smfpimcc  47636  smflimmpt  47638  smfsupmpt  47643  smfsupxr  47644  smfinfmpt  47647  smflimsuplem2  47649  smflimsuplem7  47654  smflimsupmpt  47657  smfliminfmpt  47660  cfsetsnfsetf  47946  1arymaptfo  49573  2arymaptfo  49584  setrec2mpt  50623  aacllem  50772