Theorem mpoex 8058

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044  Vcvv 3447   ∈ cmpo 7389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  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 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969

This theorem is referenced by:  mptmpoopabbrdOLD  8060  qexALT  12923  ruclem13  16210  vdwapfval  16942  prdsco  17431  imasvsca  17483  homffval  17651  comfffval  17659  comffval  17660  comfffn  17665  comfeq  17667  oppccofval  17677  monfval  17694  sectffval  17712  invffval  17720  cofu1st  17845  cofu2nd  17847  cofucl  17850  natfval  17911  fuccofval  17924  fucco  17927  coafval  18026  setcco  18045  catchomfval  18064  catccofval  18066  catcco  18067  estrcco  18091  xpcval  18138  xpchomfval  18140  xpccofval  18143  xpcco  18144  1stf1  18153  1stf2  18154  2ndf1  18156  2ndf2  18157  1stfcl  18158  2ndfcl  18159  prf1  18161  prf2fval  18162  prfcl  18164  prf1st  18165  prf2nd  18166  evlf2  18179  evlf1  18181  evlfcl  18183  curf1fval  18185  curf11  18187  curf12  18188  curf1cl  18189  curf2  18190  curfcl  18193  hof1fval  18214  hof2fval  18216  hofcl  18220  yonedalem3  18241  efmndplusg  18807  mgmnsgrpex  18858  sgrpnmndex  18859  grpsubfvalALT  18916  mulgfvalALT  19002  symgvalstruct  19327  lsmfval  19568  pj1fval  19624  dvrfval  20311  psrmulr  21851  psrvscafval  21857  evlslem2  21986  mamufval  22279  mvmulfval  22429  isphtpy  24880  pcofval  24910  q1pval  26060  r1pval  26063  mulsproplem9  28027  motplusg  28469  midf  28703  ismidb  28705  ttgval  28802  ebtwntg  28909  ecgrtg  28910  elntg  28911  wwlksnon  29781  wspthsnon  29782  clwwlknonmpo  30018  vsfval  30562  dipfval  30631  idlsrgmulr  33478  smatfval  33785  lmatval  33803  qqhval  33962  dya2iocuni  34274  sxbrsigalem5  34279  sitmval  34340  signswplusg  34546  reprval  34601  mclsrcl  35548  mclsval  35550  ldualfvs  39129  paddfval  39791  tgrpopr  40741  erngfplus  40796  erngfmul  40799  erngfplus-rN  40804  erngfmul-rN  40807  dvafvadd  41008  dvafvsca  41010  dvaabl  41018  dvhfvadd  41085  dvhfvsca  41094  djafvalN  41128  djhfval  41391  hlhilip  41942  mendplusgfval  43170  mendmulrfval  43172  mendvscafval  43175  mnringmulrd  44212  mnringmulrcld  44217  hoidmvval  46575  cznrng  48249  cznnring  48250  rngchomfvalALTV  48255  rngccofvalALTV  48258  rngccoALTV  48259  ringchomfvalALTV  48289  ringccofvalALTV  48292  ringccoALTV  48293  rrx2xpreen  48708  lines  48720  spheres  48735  funcf2lem2  49071  upfval  49165  swapfelvv  49252  swapf2fvala  49253  swapf1vala  49255  tposcurf1  49288  diag1f1lem  49295  fucoelvv  49309  fucofn2  49313  fucofvalne  49314  fuco112  49318  fuco111  49319  fuco21  49325  prcofelvv  49369  reldmprcof1  49370  reldmprcof2  49371  prcof1  49377  prcof2a  49378  prcof2  49379  functhinclem1  49433  thincciso  49442  functermc2  49498  incat  49590  setc1onsubc  49591  lanfn  49598  ranfn  49599  lanfval  49602  ranfval  49603