Theorem mpoex 8104

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

Syntax hints:   ∈ wcel 2108  ∀wral 3061  Vcvv 3480   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015

This theorem is referenced by:  mptmpoopabbrdOLD  8106  qexALT  13006  ruclem13  16278  vdwapfval  17009  prdsco  17513  imasvsca  17565  homffval  17733  comfffval  17741  comffval  17742  comfffn  17747  comfeq  17749  oppccofval  17759  monfval  17776  sectffval  17794  invffval  17802  cofu1st  17928  cofu2nd  17930  cofucl  17933  natfval  17994  fuccofval  18007  fucco  18010  coafval  18109  setcco  18128  catchomfval  18147  catccofval  18149  catcco  18150  estrcco  18174  xpcval  18222  xpchomfval  18224  xpccofval  18227  xpcco  18228  1stf1  18237  1stf2  18238  2ndf1  18240  2ndf2  18241  1stfcl  18242  2ndfcl  18243  prf1  18245  prf2fval  18246  prfcl  18248  prf1st  18249  prf2nd  18250  evlf2  18263  evlf1  18265  evlfcl  18267  curf1fval  18269  curf11  18271  curf12  18272  curf1cl  18273  curf2  18274  curfcl  18277  hof1fval  18298  hof2fval  18300  hofcl  18304  yonedalem3  18325  efmndplusg  18893  mgmnsgrpex  18944  sgrpnmndex  18945  grpsubfvalALT  19002  mulgfvalALT  19088  symgvalstruct  19414  symgvalstructOLD  19415  lsmfval  19656  pj1fval  19712  dvrfval  20402  psrmulr  21962  psrvscafval  21968  evlslem2  22103  mamufval  22396  mvmulfval  22548  isphtpy  25013  pcofval  25043  q1pval  26194  r1pval  26197  mulsproplem9  28150  motplusg  28550  midf  28784  ismidb  28786  ttgval  28883  ttgvalOLD  28884  ebtwntg  28997  ecgrtg  28998  elntg  28999  wwlksnon  29871  wspthsnon  29872  clwwlknonmpo  30108  vsfval  30652  dipfval  30721  idlsrgmulr  33535  smatfval  33794  lmatval  33812  qqhval  33973  dya2iocuni  34285  sxbrsigalem5  34290  sitmval  34351  signswplusg  34570  reprval  34625  mclsrcl  35566  mclsval  35568  ldualfvs  39137  paddfval  39799  tgrpopr  40749  erngfplus  40804  erngfmul  40807  erngfplus-rN  40812  erngfmul-rN  40815  dvafvadd  41016  dvafvsca  41018  dvaabl  41026  dvhfvadd  41093  dvhfvsca  41102  djafvalN  41136  djhfval  41399  hlhilip  41954  mendplusgfval  43193  mendmulrfval  43195  mendvscafval  43198  mnringmulrd  44240  mnringmulrcld  44247  hoidmvval  46592  cznrng  48177  cznnring  48178  rngchomfvalALTV  48183  rngccofvalALTV  48186  rngccoALTV  48187  ringchomfvalALTV  48217  ringccofvalALTV  48220  ringccoALTV  48221  rrx2xpreen  48640  lines  48652  spheres  48667  funcf2lem2  48915  upfval  48933  swapfelvv  48969  swapf2fvala  48970  swapf1vala  48972  tposcurf1  48999  fucoelvv  49015  fucofn2  49019  fucofvalne  49020  fuco112  49024  fuco111  49025  fuco21  49031  functhinclem1  49093  thincciso  49102  functermc2  49141