Theorem mpoex 8017

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

Syntax hints:   ∈ wcel 2106  ∀wral 3060  Vcvv 3446   ∈ cmpo 7364

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 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927

This theorem is referenced by:  mptmpoopabbrd  8018  qexALT  12898  ruclem13  16135  vdwapfval  16854  prdsco  17364  imasvsca  17416  homffval  17584  comfffval  17592  comffval  17593  comfffn  17598  comfeq  17600  oppccofval  17611  monfval  17629  sectffval  17647  invffval  17655  cofu1st  17783  cofu2nd  17785  cofucl  17788  natfval  17847  fuccofval  17861  fucco  17865  coafval  17964  setcco  17983  catchomfval  18002  catccofval  18004  catcco  18005  estrcco  18031  xpcval  18079  xpchomfval  18081  xpccofval  18084  xpcco  18085  1stf1  18094  1stf2  18095  2ndf1  18097  2ndf2  18098  1stfcl  18099  2ndfcl  18100  prf1  18102  prf2fval  18103  prfcl  18105  prf1st  18106  prf2nd  18107  evlf2  18121  evlf1  18123  evlfcl  18125  curf1fval  18127  curf11  18129  curf12  18130  curf1cl  18131  curf2  18132  curfcl  18135  hof1fval  18156  hof2fval  18158  hofcl  18162  yonedalem3  18183  efmndplusg  18704  mgmnsgrpex  18755  sgrpnmndex  18756  grpsubfvalALT  18809  mulgfvalALT  18889  symgvalstruct  19192  symgvalstructOLD  19193  lsmfval  19434  pj1fval  19490  dvrfval  20127  psrmulr  21389  psrvscafval  21395  evlslem2  21526  mamufval  21771  mvmulfval  21928  isphtpy  24381  pcofval  24410  q1pval  25555  r1pval  25558  mulsproplem10  27431  motplusg  27547  midf  27781  ismidb  27783  ttgval  27880  ttgvalOLD  27881  ebtwntg  27994  ecgrtg  27995  elntg  27996  wwlksnon  28859  wspthsnon  28860  clwwlknonmpo  29096  vsfval  29638  dipfval  29707  idlsrgmulr  32325  smatfval  32465  lmatval  32483  qqhval  32644  dya2iocuni  32972  sxbrsigalem5  32977  sitmval  33038  signswplusg  33256  reprval  33312  mclsrcl  34242  mclsval  34244  ldualfvs  37671  paddfval  38333  tgrpopr  39283  erngfplus  39338  erngfmul  39341  erngfplus-rN  39346  erngfmul-rN  39349  dvafvadd  39550  dvafvsca  39552  dvaabl  39560  dvhfvadd  39627  dvhfvsca  39636  djafvalN  39670  djhfval  39933  hlhilip  40488  mendplusgfval  41570  mendmulrfval  41572  mendvscafval  41575  mnringmulrd  42623  mnringmulrcld  42630  hoidmvval  44938  cznrng  46373  cznnring  46374  rngchomfvalALTV  46402  rngccofvalALTV  46405  rngccoALTV  46406  ringchomfvalALTV  46465  ringccofvalALTV  46468  ringccoALTV  46469  rrx2xpreen  46925  lines  46937  spheres  46952  functhinclem1  47181  thincciso  47189