Theorem nfmpt1 5246

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

Syntax hints:   ∧ wa 395   = wceq 1533   ∈ wcel 2098  Ⅎwnfc 2875  {copab 5200   ↦ cmpt 5221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-opab 5201  df-mpt 5222

This theorem is referenced by:  nffvmpt1  6892  fvmptss  7000  fvmptd3f  7003  mpteqb  7007  fvmptf  7009  ralrnmptw  7085  ralrnmpt  7087  f1ompt  7102  fompt  7109  f1mpt  7252  fliftfun  7301  rdgsucmptf  8423  rdgsucmptnf  8424  frsucmpt  8433  frsucmptn  8434  dom2lem  8983  mapxpen  9138  cnfcom3clem  9695  ttrclselem1  9715  ttrclselem2  9716  infxpenc2lem2  10010  dfac8clem  10022  acnlem  10038  fin23lem32  10334  axcc3  10428  ac6num  10469  nfcprod1  15850  yonedalem4b  18228  prdsgsum  19886  cayleyhamilton1  22704  neiptopreu  22947  2ndcdisj  23270  ptcnp  23436  cnmpt11  23477  cnmptk2  23500  xkocnv  23628  utopsnneiplem  24062  restmetu  24389  mbfposr  25491  mbfsup  25503  itg1climres  25554  itg2splitlem  25588  itg2split  25589  itg2cnlem1  25601  nfitg1  25613  dvlipcn  25837  lhop2  25858  dvfsumabs  25867  itgparts  25892  itgsubstlem  25893  itgulm2  26250  lgamgulm2  26872  lgseisenlem2  27213  istrkg2ld  28135  cnlnadjlem5  31748  acunirnmpt2  32309  acunirnmpt2f  32310  aciunf1lem  32311  ofpreima  32314  fnpreimac  32320  disjdsct  32348  fpwrelmap  32382  nsgqusf1olem1  32955  nsgqusf1olem3  32957  elrspunidl  32977  fedgmullem2  33160  locfinreflem  33275  prodindf  33476  nfesum1  33493  esumc  33504  esumrnmpt2  33521  esumsup  33542  esumgect  33543  esum2d  33546  sigapildsys  33615  ldgenpisyslem1  33616  voliune  33682  oms0  33751  rrvadd  33906  ballotlem7  33989  breprexplema  34097  cvmcov  34709  rdgssun  36715  exrecfnlem  36716  phpreu  36928  matunitlindflem2  36941  poimirlem16  36960  poimirlem19  36963  itg2addnclem  36995  ftc1anclem5  37021  totbndbnd  37113  pwsgprod  41569  mzpsubmpt  41936  eq0rabdioph  41969  eqrabdioph  41970  aomclem8  42258  binomcxplemdvbinom  43567  binomcxplemdvsum  43569  binomcxplemnotnn0  43570  refsumcn  44169  refsum2cnlem1  44176  disjrnmpt2  44338  disjf1o  44341  disjinfi  44342  choicefi  44350  axccdom  44372  rnmptbd2lem  44403  infnsuprnmpt  44405  rnmptbdlem  44410  rnmptss2  44412  rnmptssbi  44416  supxrleubrnmpt  44567  suprleubrnmpt  44583  infrnmptle  44584  infxrunb3rnmpt  44589  uzub  44592  supminfrnmpt  44606  infxrgelbrnmpt  44615  infrpgernmpt  44626  supminfxrrnmpt  44632  fmuldfeqlem1  44749  fmuldfeq  44750  climneg  44777  climdivf  44779  mullimc  44783  idlimc  44793  sumnnodd  44797  neglimc  44814  addlimc  44815  0ellimcdiv  44816  fnlimfvre  44841  fnlimabslt  44846  climreclmpt  44851  climfveqmpt2  44860  climeldmeqmpt2  44862  climeqmpt  44864  limsupubuz  44880  climinfmpt  44882  limsupubuzmpt  44886  limsupequzmptlem  44895  limsupre2mpt  44897  limsupre3mpt  44901  limsupreuzmpt  44906  liminflelimsuplem  44942  liminfvalxr  44950  liminfvalxrmpt  44953  liminfltlem  44971  liminflbuz2  44982  liminfpnfuz  44983  xlimmnfmpt  45010  xlimpnfmpt  45011  xlimpnfxnegmnf2  45025  cncfmptssg  45038  cncfshift  45041  cncficcgt0  45055  cncfiooicclem1  45060  dvnmul  45110  dvmptfprod  45112  itgsin0pilem1  45117  ibliccsinexp  45118  itgsinexplem1  45121  itgsinexp  45122  iblspltprt  45140  itgsubsticclem  45142  stoweidlem16  45183  stoweidlem18  45185  stoweidlem19  45186  stoweidlem20  45187  stoweidlem22  45189  stoweidlem23  45190  stoweidlem27  45194  stoweidlem31  45198  stoweidlem32  45199  stoweidlem34  45201  stoweidlem35  45202  stoweidlem36  45203  stoweidlem40  45207  stoweidlem41  45208  stoweidlem42  45209  stoweidlem43  45210  stoweidlem44  45211  stoweidlem45  45212  stoweidlem48  45215  stoweidlem51  45218  stoweidlem55  45222  stoweidlem59  45226  stoweidlem60  45227  stoweidlem62  45229  wallispilem5  45236  stirlinglem4  45244  stirlinglem5  45245  stirlinglem8  45248  stirlinglem11  45251  stirlinglem12  45252  stirlinglem13  45253  stirlinglem14  45254  stirlinglem15  45255  stirling  45256  fourierdlem16  45290  fourierdlem21  45295  fourierdlem22  45296  fourierdlem68  45341  fourierdlem73  45346  fourierdlem80  45353  fourierdlem89  45362  fourierdlem91  45364  fourierdlem93  45366  fourierdlem103  45376  fourierdlem104  45377  fourierdlem112  45385  fourierdlem115  45388  fourierd  45389  fourierclimd  45390  etransclem48  45449  sge00  45543  sge0revalmpt  45545  sge0f1o  45549  sge0fsummpt  45557  sge0gerp  45562  sge0pnffigt  45563  sge0lefi  45565  sge0ltfirp  45567  sge0resplit  45573  sge0iunmptlemfi  45580  sge0iunmpt  45585  sge0xadd  45602  sge0fsummptf  45603  sge0gtfsumgt  45610  sge0reuz  45614  iundjiun  45627  meaiuninc3v  45651  omeiunltfirp  45686  omeiunlempt  45687  hoicvrrex  45723  ovncvrrp  45731  ovnhoilem1  45768  ovnlecvr2  45777  opnvonmbllem1  45799  iunhoiioolem  45842  smfpimltmpt  45913  issmfdmpt  45915  smfconst  45916  smfpimltxrmptf  45925  smflimlem2  45939  smflim  45944  smfpimgtmpt  45948  smfpimgtxrmptf  45951  smfpimcclem  45974  smfpimcc  45975  smflimmpt  45977  smfsupmpt  45982  smfsupxr  45983  smfinfmpt  45986  smflimsuplem2  45988  smflimsuplem7  45993  smflimsupmpt  45996  smfliminfmpt  45999  cfsetsnfsetf  46219  1arymaptfo  47483  2arymaptfo  47494  setrec2mpt  47896  aacllem  48002