Theorem mpoex 8072

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

Syntax hints:   ∈ wcel 2149  ∀wral 3085  Vcvv 3463   ∈ cmpo 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-oprab 7412  df-mpo 7413  df-1st 7982  df-2nd 7983

This theorem is referenced by:  qexALT  12984  ruclem13  16294  vdwapfval  17027  prdsco  17517  imasvsca  17570  homffval  17742  comfffval  17750  comffval  17751  comfffn  17756  comfeq  17758  oppccofval  17768  monfval  17785  sectffval  17803  invffval  17811  cofu1st  17936  cofu2nd  17938  cofucl  17941  natfval  18002  fuccofval  18015  fucco  18018  coafval  18117  setcco  18136  catchomfval  18155  catccofval  18157  catcco  18158  estrcco  18182  xpcval  18229  xpchomfval  18231  xpccofval  18234  xpcco  18235  1stf1  18244  1stf2  18245  2ndf1  18247  2ndf2  18248  1stfcl  18249  2ndfcl  18250  prf1  18252  prf2fval  18253  prfcl  18255  prf1st  18256  prf2nd  18257  evlf2  18270  evlf1  18272  evlfcl  18274  curf1fval  18276  curf11  18278  curf12  18279  curf1cl  18280  curf2  18281  curfcl  18284  hof1fval  18305  hof2fval  18307  hofcl  18311  yonedalem3  18332  efmndplusg  18935  mgmnsgrpex  18989  sgrpnmndex  18990  grpsubfvalALT  19047  mulgfvalALT  19132  symgvalstruct  19463  lsmfval  19704  pj1fval  19760  dvrfval  20480  psrmulr  22057  psrvscafval  22063  evlslem2  22195  mamufval  22514  mvmulfval  22664  isphtpy  25105  pcofval  25134  q1pval  26277  r1pval  26280  mulsproplem9  28279  motplusg  28773  midf  29039  ismidb  29041  ttgval  29161  ebtwntg  29269  ecgrtg  29270  elntg  29271  wwlksnon  30137  wspthsnon  30138  clwwlknonmpo  30377  vsfval  30922  dipfval  30991  idlsrgmulr  33738  smatfval  34126  lmatval  34144  qqhval  34303  dya2iocuni  34614  sxbrsigalem5  34619  sitmval  34680  signswplusg  34883  reprval  34938  mclsrcl  35948  mclsval  35950  ldualfvs  39795  paddfval  40456  tgrpopr  41406  erngfplus  41461  erngfmul  41464  erngfplus-rN  41469  erngfmul-rN  41472  dvafvadd  41673  dvafvsca  41675  dvaabl  41683  dvhfvadd  41750  dvhfvsca  41759  djafvalN  41793  djhfval  42056  hlhilip  42607  mendplusgfval  43793  mendmulrfval  43795  mendvscafval  43798  mnringmulrd  44832  mnringmulrcld  44837  hoidmvval  47176  cznrng  48908  cznnring  48909  rngchomfvalALTV  48914  rngccofvalALTV  48917  rngccoALTV  48918  ringchomfvalALTV  48948  ringccofvalALTV  48951  ringccoALTV  48952  rrx2xpreen  49377  lines  49389  spheres  49404  funcf2lem2  49738  upfval  49832  swapfelvv  49919  swapf2fvala  49920  swapf1vala  49922  tposcurf1  49955  diag1f1lem  49962  fucoelvv  49976  fucofn2  49980  fucofvalne  49981  fuco112  49985  fuco111  49986  fuco21  49992  prcofelvv  50036  reldmprcof1  50037  reldmprcof2  50038  prcof1  50044  prcof2a  50045  prcof2  50046  functhinclem1  50100  thincciso  50109  functermc2  50165  incat  50257  setc1onsubc  50258  lanfn  50265  ranfn  50266  lanfval  50269  ranfval  50270