Theorem mpoex 8078

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

Syntax hints:   ∈ wcel 2108  ∀wral 3051  Vcvv 3459   ∈ cmpo 7407

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-oprab 7409  df-mpo 7410  df-1st 7988  df-2nd 7989

This theorem is referenced by:  mptmpoopabbrdOLD  8080  qexALT  12980  ruclem13  16260  vdwapfval  16991  prdsco  17482  imasvsca  17534  homffval  17702  comfffval  17710  comffval  17711  comfffn  17716  comfeq  17718  oppccofval  17728  monfval  17745  sectffval  17763  invffval  17771  cofu1st  17896  cofu2nd  17898  cofucl  17901  natfval  17962  fuccofval  17975  fucco  17978  coafval  18077  setcco  18096  catchomfval  18115  catccofval  18117  catcco  18118  estrcco  18142  xpcval  18189  xpchomfval  18191  xpccofval  18194  xpcco  18195  1stf1  18204  1stf2  18205  2ndf1  18207  2ndf2  18208  1stfcl  18209  2ndfcl  18210  prf1  18212  prf2fval  18213  prfcl  18215  prf1st  18216  prf2nd  18217  evlf2  18230  evlf1  18232  evlfcl  18234  curf1fval  18236  curf11  18238  curf12  18239  curf1cl  18240  curf2  18241  curfcl  18244  hof1fval  18265  hof2fval  18267  hofcl  18271  yonedalem3  18292  efmndplusg  18858  mgmnsgrpex  18909  sgrpnmndex  18910  grpsubfvalALT  18967  mulgfvalALT  19053  symgvalstruct  19378  lsmfval  19619  pj1fval  19675  dvrfval  20362  psrmulr  21902  psrvscafval  21908  evlslem2  22037  mamufval  22330  mvmulfval  22480  isphtpy  24931  pcofval  24961  q1pval  26112  r1pval  26115  mulsproplem9  28079  motplusg  28521  midf  28755  ismidb  28757  ttgval  28854  ebtwntg  28961  ecgrtg  28962  elntg  28963  wwlksnon  29833  wspthsnon  29834  clwwlknonmpo  30070  vsfval  30614  dipfval  30683  idlsrgmulr  33522  smatfval  33826  lmatval  33844  qqhval  34003  dya2iocuni  34315  sxbrsigalem5  34320  sitmval  34381  signswplusg  34587  reprval  34642  mclsrcl  35583  mclsval  35585  ldualfvs  39154  paddfval  39816  tgrpopr  40766  erngfplus  40821  erngfmul  40824  erngfplus-rN  40829  erngfmul-rN  40832  dvafvadd  41033  dvafvsca  41035  dvaabl  41043  dvhfvadd  41110  dvhfvsca  41119  djafvalN  41153  djhfval  41416  hlhilip  41967  mendplusgfval  43205  mendmulrfval  43207  mendvscafval  43210  mnringmulrd  44247  mnringmulrcld  44252  hoidmvval  46606  cznrng  48236  cznnring  48237  rngchomfvalALTV  48242  rngccofvalALTV  48245  rngccoALTV  48246  ringchomfvalALTV  48276  ringccofvalALTV  48279  ringccoALTV  48280  rrx2xpreen  48699  lines  48711  spheres  48726  funcf2lem2  49047  upfval  49111  swapfelvv  49180  swapf2fvala  49181  swapf1vala  49183  tposcurf1  49210  diag1f1lem  49217  fucoelvv  49231  fucofn2  49235  fucofvalne  49236  fuco112  49240  fuco111  49241  fuco21  49247  prcofelvv  49290  reldmprcof1  49291  reldmprcof2  49292  prcof1  49298  prcof2a  49299  prcof2  49300  functhinclem1  49330  thincciso  49339  functermc2  49394  incat  49478  setc1onsubc  49479  lanfn  49486  ranfn  49487  lanfval  49490  ranfval  49491