Theorem mpoex 7906

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

Syntax hints:   ∈ wcel 2109  ∀wral 3065  Vcvv 3430   ∈ cmpo 7270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-oprab 7272  df-mpo 7273  df-1st 7817  df-2nd 7818

This theorem is referenced by:  qexALT  12686  ruclem13  15932  vdwapfval  16653  prdsco  17160  imasvsca  17212  homffval  17380  comfffval  17388  comffval  17389  comfffn  17394  comfeq  17396  oppccofval  17407  monfval  17425  sectffval  17443  invffval  17451  cofu1st  17579  cofu2nd  17581  cofucl  17584  natfval  17643  fuccofval  17657  fucco  17661  coafval  17760  setcco  17779  catchomfval  17798  catccofval  17800  catcco  17801  estrcco  17827  xpcval  17875  xpchomfval  17877  xpccofval  17880  xpcco  17881  1stf1  17890  1stf2  17891  2ndf1  17893  2ndf2  17894  1stfcl  17895  2ndfcl  17896  prf1  17898  prf2fval  17899  prfcl  17901  prf1st  17902  prf2nd  17903  evlf2  17917  evlf1  17919  evlfcl  17921  curf1fval  17923  curf11  17925  curf12  17926  curf1cl  17927  curf2  17928  curfcl  17931  hof1fval  17952  hof2fval  17954  hofcl  17958  yonedalem3  17979  efmndplusg  18500  mgmnsgrpex  18551  sgrpnmndex  18552  grpsubfvalALT  18605  mulgfvalALT  18684  symgvalstruct  18985  symgvalstructOLD  18986  lsmfval  19224  pj1fval  19281  dvrfval  19907  psrmulr  21134  psrvscafval  21140  evlslem2  21270  mamufval  21515  mvmulfval  21672  isphtpy  24125  pcofval  24154  q1pval  25299  r1pval  25302  motplusg  26884  midf  27118  ismidb  27120  ttgval  27217  ttgvalOLD  27218  ebtwntg  27331  ecgrtg  27332  elntg  27333  wwlksnon  28195  wspthsnon  28196  clwwlknonmpo  28432  vsfval  28974  dipfval  29043  idlsrgmulr  31631  smatfval  31724  lmatval  31742  qqhval  31903  dya2iocuni  32229  sxbrsigalem5  32234  sitmval  32295  signswplusg  32513  reprval  32569  mclsrcl  33502  mclsval  33504  ldualfvs  37129  paddfval  37790  tgrpopr  38740  erngfplus  38795  erngfmul  38798  erngfplus-rN  38803  erngfmul-rN  38806  dvafvadd  39007  dvafvsca  39009  dvaabl  39017  dvhfvadd  39084  dvhfvsca  39093  djafvalN  39127  djhfval  39390  hlhilip  39945  mendplusgfval  40990  mendmulrfval  40992  mendvscafval  40995  mnringmulrd  41792  mnringmulrcld  41799  hoidmvval  44069  cznrng  45465  cznnring  45466  rngchomfvalALTV  45494  rngccofvalALTV  45497  rngccoALTV  45498  ringchomfvalALTV  45557  ringccofvalALTV  45560  ringccoALTV  45561  rrx2xpreen  46017  lines  46029  spheres  46044  functhinclem1  46274  thincciso  46282