Theorem mpoex 8068

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 3065	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		eqid 2732	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
5	4	mpoexxg 8064	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)
6	1, 3, 5	mp2an 690	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

Syntax hints:   ∈ wcel 2106  ∀wral 3061  Vcvv 3474   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978

This theorem is referenced by:  mptmpoopabbrd  8069  qexALT  12952  ruclem13  16189  vdwapfval  16908  prdsco  17418  imasvsca  17470  homffval  17638  comfffval  17646  comffval  17647  comfffn  17652  comfeq  17654  oppccofval  17665  monfval  17683  sectffval  17701  invffval  17709  cofu1st  17837  cofu2nd  17839  cofucl  17842  natfval  17901  fuccofval  17915  fucco  17919  coafval  18018  setcco  18037  catchomfval  18056  catccofval  18058  catcco  18059  estrcco  18085  xpcval  18133  xpchomfval  18135  xpccofval  18138  xpcco  18139  1stf1  18148  1stf2  18149  2ndf1  18151  2ndf2  18152  1stfcl  18153  2ndfcl  18154  prf1  18156  prf2fval  18157  prfcl  18159  prf1st  18160  prf2nd  18161  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  18797  mgmnsgrpex  18848  sgrpnmndex  18849  grpsubfvalALT  18905  mulgfvalALT  18989  symgvalstruct  19305  symgvalstructOLD  19306  lsmfval  19547  pj1fval  19603  dvrfval  20293  psrmulr  21722  psrvscafval  21728  evlslem2  21861  mamufval  22107  mvmulfval  22264  isphtpy  24721  pcofval  24750  q1pval  25895  r1pval  25898  mulsproplem9  27807  motplusg  28048  midf  28282  ismidb  28284  ttgval  28381  ttgvalOLD  28382  ebtwntg  28495  ecgrtg  28496  elntg  28497  wwlksnon  29360  wspthsnon  29361  clwwlknonmpo  29597  vsfval  30141  dipfval  30210  idlsrgmulr  32883  smatfval  33061  lmatval  33079  qqhval  33240  dya2iocuni  33568  sxbrsigalem5  33573  sitmval  33634  signswplusg  33852  reprval  33908  mclsrcl  34838  mclsval  34840  ldualfvs  38309  paddfval  38971  tgrpopr  39921  erngfplus  39976  erngfmul  39979  erngfplus-rN  39984  erngfmul-rN  39987  dvafvadd  40188  dvafvsca  40190  dvaabl  40198  dvhfvadd  40265  dvhfvsca  40274  djafvalN  40308  djhfval  40571  hlhilip  41126  mendplusgfval  42229  mendmulrfval  42231  mendvscafval  42234  mnringmulrd  43282  mnringmulrcld  43289  hoidmvval  45592  cznrng  46942  cznnring  46943  rngchomfvalALTV  46971  rngccofvalALTV  46974  rngccoALTV  46975  ringchomfvalALTV  47034  ringccofvalALTV  47037  ringccoALTV  47038  rrx2xpreen  47493  lines  47505  spheres  47520  functhinclem1  47749  thincciso  47757