Theorem nfmpt1 5256

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

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2106  Ⅎwnfc 2888  {copab 5210   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-opab 5211  df-mpt 5232

This theorem is referenced by:  nffvmpt1  6918  fvmptss  7028  fvmptd3f  7031  mpteqb  7035  fvmptf  7037  ralrnmptw  7114  ralrnmpt  7116  f1ompt  7131  fompt  7138  f1mpt  7281  fliftfun  7332  rdgsucmptf  8467  rdgsucmptnf  8468  frsucmpt  8477  frsucmptn  8478  dom2lem  9031  mapxpen  9182  cnfcom3clem  9743  ttrclselem1  9763  ttrclselem2  9764  infxpenc2lem2  10058  dfac8clem  10070  acnlem  10086  fin23lem32  10382  axcc3  10476  ac6num  10517  nfcprod1  15941  yonedalem4b  18333  prdsgsum  20014  cayleyhamilton1  22914  neiptopreu  23157  2ndcdisj  23480  ptcnp  23646  cnmpt11  23687  cnmptk2  23710  xkocnv  23838  utopsnneiplem  24272  restmetu  24599  mbfposr  25701  mbfsup  25713  itg1climres  25764  itg2splitlem  25798  itg2split  25799  itg2cnlem1  25811  nfitg1  25824  dvlipcn  26048  lhop2  26069  dvfsumabs  26078  itgparts  26103  itgsubstlem  26104  itgulm2  26467  lgamgulm2  27094  lgseisenlem2  27435  istrkg2ld  28483  cnlnadjlem5  32100  acunirnmpt2  32677  acunirnmpt2f  32678  aciunf1lem  32679  ofpreima  32682  fnpreimac  32688  disjdsct  32718  fpwrelmap  32751  nsgqusf1olem1  33421  nsgqusf1olem3  33423  elrspunidl  33436  fedgmullem2  33658  locfinreflem  33801  prodindf  34004  nfesum1  34021  esumc  34032  esumrnmpt2  34049  esumsup  34070  esumgect  34071  esum2d  34074  sigapildsys  34143  ldgenpisyslem1  34144  voliune  34210  oms0  34279  rrvadd  34434  ballotlem7  34517  breprexplema  34624  cvmcov  35248  rdgssun  37361  exrecfnlem  37362  phpreu  37591  matunitlindflem2  37604  poimirlem16  37623  poimirlem19  37626  itg2addnclem  37658  ftc1anclem5  37684  totbndbnd  37776  pwsgprod  42531  mzpsubmpt  42731  eq0rabdioph  42764  eqrabdioph  42765  aomclem8  43050  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  refsumcn  44968  refsum2cnlem1  44975  disjrnmpt2  45131  disjf1o  45134  disjinfi  45135  choicefi  45143  axccdom  45165  rnmptbd2lem  45193  infnsuprnmpt  45195  rnmptbdlem  45200  rnmptss2  45202  rnmptssbi  45206  supxrleubrnmpt  45356  suprleubrnmpt  45372  infrnmptle  45373  infxrunb3rnmpt  45378  uzub  45381  supminfrnmpt  45395  infxrgelbrnmpt  45404  infrpgernmpt  45415  supminfxrrnmpt  45421  fmuldfeqlem1  45538  fmuldfeq  45539  climneg  45566  climdivf  45568  mullimc  45572  idlimc  45582  sumnnodd  45586  neglimc  45603  addlimc  45604  0ellimcdiv  45605  fnlimfvre  45630  fnlimabslt  45635  climreclmpt  45640  climfveqmpt2  45649  climeldmeqmpt2  45651  climeqmpt  45653  limsupubuz  45669  climinfmpt  45671  limsupubuzmpt  45675  limsupequzmptlem  45684  limsupre2mpt  45686  limsupre3mpt  45690  limsupreuzmpt  45695  liminflelimsuplem  45731  liminfvalxr  45739  liminfvalxrmpt  45742  liminfltlem  45760  liminflbuz2  45771  liminfpnfuz  45772  xlimmnfmpt  45799  xlimpnfmpt  45800  xlimpnfxnegmnf2  45814  cncfmptssg  45827  cncfshift  45830  cncficcgt0  45844  cncfiooicclem1  45849  dvnmul  45899  dvmptfprod  45901  itgsin0pilem1  45906  ibliccsinexp  45907  itgsinexplem1  45910  itgsinexp  45911  iblspltprt  45929  itgsubsticclem  45931  stoweidlem16  45972  stoweidlem18  45974  stoweidlem19  45975  stoweidlem20  45976  stoweidlem22  45978  stoweidlem23  45979  stoweidlem27  45983  stoweidlem31  45987  stoweidlem32  45988  stoweidlem34  45990  stoweidlem35  45991  stoweidlem36  45992  stoweidlem40  45996  stoweidlem41  45997  stoweidlem42  45998  stoweidlem43  45999  stoweidlem44  46000  stoweidlem45  46001  stoweidlem48  46004  stoweidlem51  46007  stoweidlem55  46011  stoweidlem59  46015  stoweidlem60  46016  stoweidlem62  46018  wallispilem5  46025  stirlinglem4  46033  stirlinglem5  46034  stirlinglem8  46037  stirlinglem11  46040  stirlinglem12  46041  stirlinglem13  46042  stirlinglem14  46043  stirlinglem15  46044  stirling  46045  fourierdlem16  46079  fourierdlem21  46084  fourierdlem22  46085  fourierdlem68  46130  fourierdlem73  46135  fourierdlem80  46142  fourierdlem89  46151  fourierdlem91  46153  fourierdlem93  46155  fourierdlem103  46165  fourierdlem104  46166  fourierdlem112  46174  fourierdlem115  46177  fourierd  46178  fourierclimd  46179  etransclem48  46238  sge00  46332  sge0revalmpt  46334  sge0f1o  46338  sge0fsummpt  46346  sge0gerp  46351  sge0pnffigt  46352  sge0lefi  46354  sge0ltfirp  46356  sge0resplit  46362  sge0iunmptlemfi  46369  sge0iunmpt  46374  sge0xadd  46391  sge0fsummptf  46392  sge0gtfsumgt  46399  sge0reuz  46403  iundjiun  46416  meaiuninc3v  46440  omeiunltfirp  46475  omeiunlempt  46476  hoicvrrex  46512  ovncvrrp  46520  ovnhoilem1  46557  ovnlecvr2  46566  opnvonmbllem1  46588  iunhoiioolem  46631  smfpimltmpt  46702  issmfdmpt  46704  smfconst  46705  smfpimltxrmptf  46714  smflimlem2  46728  smflim  46733  smfpimgtmpt  46737  smfpimgtxrmptf  46740  smfpimcclem  46763  smfpimcc  46764  smflimmpt  46766  smfsupmpt  46771  smfsupxr  46772  smfinfmpt  46775  smflimsuplem2  46777  smflimsuplem7  46782  smflimsupmpt  46785  smfliminfmpt  46788  cfsetsnfsetf  47008  1arymaptfo  48493  2arymaptfo  48504  setrec2mpt  48928  aacllem  49032