Theorem mpoex 8048

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

Syntax hints:   ∈ wcel 2106  ∀wral 3060  Vcvv 3473   ∈ cmpo 7395

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-oprab 7397  df-mpo 7398  df-1st 7957  df-2nd 7958

This theorem is referenced by:  mptmpoopabbrd  8049  qexALT  12930  ruclem13  16167  vdwapfval  16886  prdsco  17396  imasvsca  17448  homffval  17616  comfffval  17624  comffval  17625  comfffn  17630  comfeq  17632  oppccofval  17643  monfval  17661  sectffval  17679  invffval  17687  cofu1st  17815  cofu2nd  17817  cofucl  17820  natfval  17879  fuccofval  17893  fucco  17897  coafval  17996  setcco  18015  catchomfval  18034  catccofval  18036  catcco  18037  estrcco  18063  xpcval  18111  xpchomfval  18113  xpccofval  18116  xpcco  18117  1stf1  18126  1stf2  18127  2ndf1  18129  2ndf2  18130  1stfcl  18131  2ndfcl  18132  prf1  18134  prf2fval  18135  prfcl  18137  prf1st  18138  prf2nd  18139  evlf2  18153  evlf1  18155  evlfcl  18157  curf1fval  18159  curf11  18161  curf12  18162  curf1cl  18163  curf2  18164  curfcl  18167  hof1fval  18188  hof2fval  18190  hofcl  18194  yonedalem3  18215  efmndplusg  18736  mgmnsgrpex  18787  sgrpnmndex  18788  grpsubfvalALT  18844  mulgfvalALT  18925  symgvalstruct  19228  symgvalstructOLD  19229  lsmfval  19470  pj1fval  19526  dvrfval  20166  psrmulr  21434  psrvscafval  21440  evlslem2  21571  mamufval  21816  mvmulfval  21973  isphtpy  24426  pcofval  24455  q1pval  25600  r1pval  25603  mulsproplem9  27493  motplusg  27658  midf  27892  ismidb  27894  ttgval  27991  ttgvalOLD  27992  ebtwntg  28105  ecgrtg  28106  elntg  28107  wwlksnon  28970  wspthsnon  28971  clwwlknonmpo  29207  vsfval  29749  dipfval  29818  idlsrgmulr  32466  smatfval  32606  lmatval  32624  qqhval  32785  dya2iocuni  33113  sxbrsigalem5  33118  sitmval  33179  signswplusg  33397  reprval  33453  mclsrcl  34383  mclsval  34385  ldualfvs  37811  paddfval  38473  tgrpopr  39423  erngfplus  39478  erngfmul  39481  erngfplus-rN  39486  erngfmul-rN  39489  dvafvadd  39690  dvafvsca  39692  dvaabl  39700  dvhfvadd  39767  dvhfvsca  39776  djafvalN  39810  djhfval  40073  hlhilip  40628  mendplusgfval  41698  mendmulrfval  41700  mendvscafval  41703  mnringmulrd  42751  mnringmulrcld  42758  hoidmvval  45066  cznrng  46501  cznnring  46502  rngchomfvalALTV  46530  rngccofvalALTV  46533  rngccoALTV  46534  ringchomfvalALTV  46593  ringccofvalALTV  46596  ringccoALTV  46597  rrx2xpreen  47053  lines  47065  spheres  47080  functhinclem1  47309  thincciso  47317