Theorem mpoex 8103

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

Syntax hints:   ∈ wcel 2106  ∀wral 3059  Vcvv 3478   ∈ cmpo 7433

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  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014

This theorem is referenced by:  mptmpoopabbrdOLD  8105  qexALT  13004  ruclem13  16275  vdwapfval  17005  prdsco  17515  imasvsca  17567  homffval  17735  comfffval  17743  comffval  17744  comfffn  17749  comfeq  17751  oppccofval  17762  monfval  17780  sectffval  17798  invffval  17806  cofu1st  17934  cofu2nd  17936  cofucl  17939  natfval  18001  fuccofval  18015  fucco  18019  coafval  18118  setcco  18137  catchomfval  18156  catccofval  18158  catcco  18159  estrcco  18185  xpcval  18233  xpchomfval  18235  xpccofval  18238  xpcco  18239  1stf1  18248  1stf2  18249  2ndf1  18251  2ndf2  18252  1stfcl  18253  2ndfcl  18254  prf1  18256  prf2fval  18257  prfcl  18259  prf1st  18260  prf2nd  18261  evlf2  18275  evlf1  18277  evlfcl  18279  curf1fval  18281  curf11  18283  curf12  18284  curf1cl  18285  curf2  18286  curfcl  18289  hof1fval  18310  hof2fval  18312  hofcl  18316  yonedalem3  18337  efmndplusg  18906  mgmnsgrpex  18957  sgrpnmndex  18958  grpsubfvalALT  19015  mulgfvalALT  19101  symgvalstruct  19429  symgvalstructOLD  19430  lsmfval  19671  pj1fval  19727  dvrfval  20419  psrmulr  21980  psrvscafval  21986  evlslem2  22121  mamufval  22412  mvmulfval  22564  isphtpy  25027  pcofval  25057  q1pval  26209  r1pval  26212  mulsproplem9  28165  motplusg  28565  midf  28799  ismidb  28801  ttgval  28898  ttgvalOLD  28899  ebtwntg  29012  ecgrtg  29013  elntg  29014  wwlksnon  29881  wspthsnon  29882  clwwlknonmpo  30118  vsfval  30662  dipfval  30731  idlsrgmulr  33515  smatfval  33756  lmatval  33774  qqhval  33935  dya2iocuni  34265  sxbrsigalem5  34270  sitmval  34331  signswplusg  34549  reprval  34604  mclsrcl  35546  mclsval  35548  ldualfvs  39118  paddfval  39780  tgrpopr  40730  erngfplus  40785  erngfmul  40788  erngfplus-rN  40793  erngfmul-rN  40796  dvafvadd  40997  dvafvsca  40999  dvaabl  41007  dvhfvadd  41074  dvhfvsca  41083  djafvalN  41117  djhfval  41380  hlhilip  41935  mendplusgfval  43170  mendmulrfval  43172  mendvscafval  43175  mnringmulrd  44217  mnringmulrcld  44224  hoidmvval  46533  cznrng  48105  cznnring  48106  rngchomfvalALTV  48111  rngccofvalALTV  48114  rngccoALTV  48115  ringchomfvalALTV  48145  ringccofvalALTV  48148  ringccoALTV  48149  rrx2xpreen  48569  lines  48581  spheres  48596  functhinclem1  48841  thincciso  48849