Theorem mpoex 8021

Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.)

Hypotheses

Ref	Expression
mpoex.1	⊢ 𝐴 ∈ V
mpoex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
mpoex	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥,𝑦)

Proof of Theorem mpoex

Step	Hyp	Ref	Expression
1		mpoex.1	. 2 ⊢ 𝐴 ∈ V
2		mpoex.2	. . 3 ⊢ 𝐵 ∈ V
3	2	rgenw 3057	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		eqid 2739	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
5	4	mpoexxg 8017	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)
6	1, 3, 5	mp2an 698	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

Syntax hints:   ∈ wcel 2119  ∀wral 3053  Vcvv 3431   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932

This theorem is referenced by:  qexALT  12905  ruclem13  16200  vdwapfval  16933  prdsco  17422  imasvsca  17475  homffval  17647  comfffval  17655  comffval  17656  comfffn  17661  comfeq  17663  oppccofval  17673  monfval  17690  sectffval  17708  invffval  17716  cofu1st  17841  cofu2nd  17843  cofucl  17846  natfval  17907  fuccofval  17920  fucco  17923  coafval  18022  setcco  18041  catchomfval  18060  catccofval  18062  catcco  18063  estrcco  18087  xpcval  18134  xpchomfval  18136  xpccofval  18139  xpcco  18140  1stf1  18149  1stf2  18150  2ndf1  18152  2ndf2  18153  1stfcl  18154  2ndfcl  18155  prf1  18157  prf2fval  18158  prfcl  18160  prf1st  18161  prf2nd  18162  evlf2  18175  evlf1  18177  evlfcl  18179  curf1fval  18181  curf11  18183  curf12  18184  curf1cl  18185  curf2  18186  curfcl  18189  hof1fval  18210  hof2fval  18212  hofcl  18216  yonedalem3  18237  efmndplusg  18839  mgmnsgrpex  18893  sgrpnmndex  18894  grpsubfvalALT  18951  mulgfvalALT  19037  symgvalstruct  19363  lsmfval  19604  pj1fval  19660  dvrfval  20373  psrmulr  21917  psrvscafval  21923  evlslem2  22055  mamufval  22375  mvmulfval  22525  isphtpy  24966  pcofval  24995  q1pval  26138  r1pval  26141  mulsproplem9  28134  motplusg  28628  midf  28862  ismidb  28864  ttgval  28961  ebtwntg  29069  ecgrtg  29070  elntg  29071  wwlksnon  29937  wspthsnon  29938  clwwlknonmpo  30177  vsfval  30722  dipfval  30791  idlsrgmulr  33590  smatfval  33979  lmatval  33997  qqhval  34156  dya2iocuni  34467  sxbrsigalem5  34472  sitmval  34533  signswplusg  34739  reprval  34794  mclsrcl  35789  mclsval  35791  ldualfvs  39628  paddfval  40289  tgrpopr  41239  erngfplus  41294  erngfmul  41297  erngfplus-rN  41302  erngfmul-rN  41305  dvafvadd  41506  dvafvsca  41508  dvaabl  41516  dvhfvadd  41583  dvhfvsca  41592  djafvalN  41626  djhfval  41889  hlhilip  42440  mendplusgfval  43626  mendmulrfval  43628  mendvscafval  43631  mnringmulrd  44667  mnringmulrcld  44672  hoidmvval  47020  cznrng  48752  cznnring  48753  rngchomfvalALTV  48758  rngccofvalALTV  48761  rngccoALTV  48762  ringchomfvalALTV  48792  ringccofvalALTV  48795  ringccoALTV  48796  rrx2xpreen  49210  lines  49222  spheres  49237  funcf2lem2  49572  upfval  49666  swapfelvv  49753  swapf2fvala  49754  swapf1vala  49756  tposcurf1  49789  diag1f1lem  49796  fucoelvv  49810  fucofn2  49814  fucofvalne  49815  fuco112  49819  fuco111  49820  fuco21  49826  prcofelvv  49870  reldmprcof1  49871  reldmprcof2  49872  prcof1  49878  prcof2a  49879  prcof2  49880  functhinclem1  49934  thincciso  49943  functermc2  49999  incat  50091  setc1onsubc  50092  lanfn  50099  ranfn  50100  lanfval  50103  ranfval  50104