Theorem mpoex 8006

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

Syntax hints:   ∈ wcel 2111  ∀wral 3047  Vcvv 3436   ∈ cmpo 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-oprab 7345  df-mpo 7346  df-1st 7916  df-2nd 7917

This theorem is referenced by:  mptmpoopabbrdOLD  8008  qexALT  12857  ruclem13  16146  vdwapfval  16878  prdsco  17367  imasvsca  17419  homffval  17591  comfffval  17599  comffval  17600  comfffn  17605  comfeq  17607  oppccofval  17617  monfval  17634  sectffval  17652  invffval  17660  cofu1st  17785  cofu2nd  17787  cofucl  17790  natfval  17851  fuccofval  17864  fucco  17867  coafval  17966  setcco  17985  catchomfval  18004  catccofval  18006  catcco  18007  estrcco  18031  xpcval  18078  xpchomfval  18080  xpccofval  18083  xpcco  18084  1stf1  18093  1stf2  18094  2ndf1  18096  2ndf2  18097  1stfcl  18098  2ndfcl  18099  prf1  18101  prf2fval  18102  prfcl  18104  prf1st  18105  prf2nd  18106  evlf2  18119  evlf1  18121  evlfcl  18123  curf1fval  18125  curf11  18127  curf12  18128  curf1cl  18129  curf2  18130  curfcl  18133  hof1fval  18154  hof2fval  18156  hofcl  18160  yonedalem3  18181  efmndplusg  18783  mgmnsgrpex  18834  sgrpnmndex  18835  grpsubfvalALT  18892  mulgfvalALT  18978  symgvalstruct  19304  lsmfval  19545  pj1fval  19601  dvrfval  20315  psrmulr  21874  psrvscafval  21880  evlslem2  22009  mamufval  22302  mvmulfval  22452  isphtpy  24902  pcofval  24932  q1pval  26082  r1pval  26085  mulsproplem9  28058  motplusg  28515  midf  28749  ismidb  28751  ttgval  28848  ebtwntg  28955  ecgrtg  28956  elntg  28957  wwlksnon  29824  wspthsnon  29825  clwwlknonmpo  30061  vsfval  30605  dipfval  30674  idlsrgmulr  33464  smatfval  33800  lmatval  33818  qqhval  33977  dya2iocuni  34288  sxbrsigalem5  34293  sitmval  34354  signswplusg  34560  reprval  34615  mclsrcl  35597  mclsval  35599  ldualfvs  39175  paddfval  39836  tgrpopr  40786  erngfplus  40841  erngfmul  40844  erngfplus-rN  40849  erngfmul-rN  40852  dvafvadd  41053  dvafvsca  41055  dvaabl  41063  dvhfvadd  41130  dvhfvsca  41139  djafvalN  41173  djhfval  41436  hlhilip  41987  mendplusgfval  43214  mendmulrfval  43216  mendvscafval  43219  mnringmulrd  44256  mnringmulrcld  44261  hoidmvval  46615  cznrng  48292  cznnring  48293  rngchomfvalALTV  48298  rngccofvalALTV  48301  rngccoALTV  48302  ringchomfvalALTV  48332  ringccofvalALTV  48335  ringccoALTV  48336  rrx2xpreen  48751  lines  48763  spheres  48778  funcf2lem2  49114  upfval  49208  swapfelvv  49295  swapf2fvala  49296  swapf1vala  49298  tposcurf1  49331  diag1f1lem  49338  fucoelvv  49352  fucofn2  49356  fucofvalne  49357  fuco112  49361  fuco111  49362  fuco21  49368  prcofelvv  49412  reldmprcof1  49413  reldmprcof2  49414  prcof1  49420  prcof2a  49421  prcof2  49422  functhinclem1  49476  thincciso  49485  functermc2  49541  incat  49633  setc1onsubc  49634  lanfn  49641  ranfn  49642  lanfval  49645  ranfval  49646