Theorem mpoex 7787

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

Syntax hints:   ∈ wcel 2111  ∀wral 3070  Vcvv 3409   ∈ cmpo 7157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-oprab 7159  df-mpo 7160  df-1st 7698  df-2nd 7699

This theorem is referenced by:  qexALT  12409  ruclem13  15648  vdwapfval  16367  prdsco  16804  imasvsca  16856  homffval  17023  comfffval  17031  comffval  17032  comfffn  17037  comfeq  17039  oppccofval  17049  monfval  17066  sectffval  17084  invffval  17092  cofu1st  17217  cofu2nd  17219  cofucl  17222  natfval  17280  fuccofval  17293  fucco  17296  coafval  17395  setcco  17414  catchomfval  17429  catccofval  17431  catcco  17432  estrcco  17451  xpcval  17498  xpchomfval  17500  xpccofval  17503  xpcco  17504  1stf1  17513  1stf2  17514  2ndf1  17516  2ndf2  17517  1stfcl  17518  2ndfcl  17519  prf1  17521  prf2fval  17522  prfcl  17524  prf1st  17525  prf2nd  17526  evlf2  17539  evlf1  17541  evlfcl  17543  curf1fval  17545  curf11  17547  curf12  17548  curf1cl  17549  curf2  17550  curfcl  17553  hof1fval  17574  hof2fval  17576  hofcl  17580  yonedalem3  17601  efmndplusg  18116  mgmnsgrpex  18167  sgrpnmndex  18168  grpsubfvalALT  18220  mulgfvalALT  18299  symgvalstruct  18597  lsmfval  18835  pj1fval  18892  dvrfval  19510  psrmulr  20717  psrvscafval  20723  evlslem2  20847  mamufval  21092  mvmulfval  21247  isphtpy  23687  pcofval  23716  q1pval  24858  r1pval  24861  motplusg  26440  midf  26674  ismidb  26676  ttgval  26773  ebtwntg  26880  ecgrtg  26881  elntg  26882  wwlksnon  27741  wspthsnon  27742  clwwlknonmpo  27978  vsfval  28520  dipfval  28589  idlsrgmulr  31177  smatfval  31270  lmatval  31288  qqhval  31447  dya2iocuni  31773  sxbrsigalem5  31778  sitmval  31839  signswplusg  32057  reprval  32113  mclsrcl  33043  mclsval  33045  ldualfvs  36738  paddfval  37399  tgrpopr  38349  erngfplus  38404  erngfmul  38407  erngfplus-rN  38412  erngfmul-rN  38415  dvafvadd  38616  dvafvsca  38618  dvaabl  38626  dvhfvadd  38693  dvhfvsca  38702  djafvalN  38736  djhfval  38999  hlhilip  39550  mendplusgfval  40530  mendmulrfval  40532  mendvscafval  40535  mnringmulrd  41332  mnringmulrcld  41337  hoidmvval  43610  cznrng  44974  cznnring  44975  rngchomfvalALTV  45003  rngccofvalALTV  45006  rngccoALTV  45007  ringchomfvalALTV  45066  ringccofvalALTV  45069  ringccoALTV  45070  rrx2xpreen  45526  lines  45538  spheres  45553