Theorem mpoex 8066

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

Syntax hints:   ∈ wcel 2107  ∀wral 3062  Vcvv 3475   ∈ cmpo 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976

This theorem is referenced by:  mptmpoopabbrd  8067  qexALT  12948  ruclem13  16185  vdwapfval  16904  prdsco  17414  imasvsca  17466  homffval  17634  comfffval  17642  comffval  17643  comfffn  17648  comfeq  17650  oppccofval  17661  monfval  17679  sectffval  17697  invffval  17705  cofu1st  17833  cofu2nd  17835  cofucl  17838  natfval  17897  fuccofval  17911  fucco  17915  coafval  18014  setcco  18033  catchomfval  18052  catccofval  18054  catcco  18055  estrcco  18081  xpcval  18129  xpchomfval  18131  xpccofval  18134  xpcco  18135  1stf1  18144  1stf2  18145  2ndf1  18147  2ndf2  18148  1stfcl  18149  2ndfcl  18150  prf1  18152  prf2fval  18153  prfcl  18155  prf1st  18156  prf2nd  18157  evlf2  18171  evlf1  18173  evlfcl  18175  curf1fval  18177  curf11  18179  curf12  18180  curf1cl  18181  curf2  18182  curfcl  18185  hof1fval  18206  hof2fval  18208  hofcl  18212  yonedalem3  18233  efmndplusg  18761  mgmnsgrpex  18812  sgrpnmndex  18813  grpsubfvalALT  18869  mulgfvalALT  18953  symgvalstruct  19264  symgvalstructOLD  19265  lsmfval  19506  pj1fval  19562  dvrfval  20216  psrmulr  21503  psrvscafval  21509  evlslem2  21642  mamufval  21887  mvmulfval  22044  isphtpy  24497  pcofval  24526  q1pval  25671  r1pval  25674  mulsproplem9  27580  motplusg  27793  midf  28027  ismidb  28029  ttgval  28126  ttgvalOLD  28127  ebtwntg  28240  ecgrtg  28241  elntg  28242  wwlksnon  29105  wspthsnon  29106  clwwlknonmpo  29342  vsfval  29886  dipfval  29955  idlsrgmulr  32621  smatfval  32775  lmatval  32793  qqhval  32954  dya2iocuni  33282  sxbrsigalem5  33287  sitmval  33348  signswplusg  33566  reprval  33622  mclsrcl  34552  mclsval  34554  mpomulex  35161  ldualfvs  38006  paddfval  38668  tgrpopr  39618  erngfplus  39673  erngfmul  39676  erngfplus-rN  39681  erngfmul-rN  39684  dvafvadd  39885  dvafvsca  39887  dvaabl  39895  dvhfvadd  39962  dvhfvsca  39971  djafvalN  40005  djhfval  40268  hlhilip  40823  mendplusgfval  41927  mendmulrfval  41929  mendvscafval  41932  mnringmulrd  42980  mnringmulrcld  42987  hoidmvval  45293  cznrng  46853  cznnring  46854  rngchomfvalALTV  46882  rngccofvalALTV  46885  rngccoALTV  46886  ringchomfvalALTV  46945  ringccofvalALTV  46948  ringccoALTV  46949  rrx2xpreen  47405  lines  47417  spheres  47432  functhinclem1  47661  thincciso  47669