Theorem mpoex 8023

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

Syntax hints:   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934

This theorem is referenced by:  mptmpoopabbrdOLD  8025  qexALT  12877  ruclem13  16167  vdwapfval  16899  prdsco  17388  imasvsca  17441  homffval  17613  comfffval  17621  comffval  17622  comfffn  17627  comfeq  17629  oppccofval  17639  monfval  17656  sectffval  17674  invffval  17682  cofu1st  17807  cofu2nd  17809  cofucl  17812  natfval  17873  fuccofval  17886  fucco  17889  coafval  17988  setcco  18007  catchomfval  18026  catccofval  18028  catcco  18029  estrcco  18053  xpcval  18100  xpchomfval  18102  xpccofval  18105  xpcco  18106  1stf1  18115  1stf2  18116  2ndf1  18118  2ndf2  18119  1stfcl  18120  2ndfcl  18121  prf1  18123  prf2fval  18124  prfcl  18126  prf1st  18127  prf2nd  18128  evlf2  18141  evlf1  18143  evlfcl  18145  curf1fval  18147  curf11  18149  curf12  18150  curf1cl  18151  curf2  18152  curfcl  18155  hof1fval  18176  hof2fval  18178  hofcl  18182  yonedalem3  18203  efmndplusg  18805  mgmnsgrpex  18856  sgrpnmndex  18857  grpsubfvalALT  18914  mulgfvalALT  19000  symgvalstruct  19326  lsmfval  19567  pj1fval  19623  dvrfval  20338  psrmulr  21898  psrvscafval  21904  evlslem2  22034  mamufval  22336  mvmulfval  22486  isphtpy  24936  pcofval  24966  q1pval  26116  r1pval  26119  mulsproplem9  28120  motplusg  28614  midf  28848  ismidb  28850  ttgval  28947  ebtwntg  29055  ecgrtg  29056  elntg  29057  wwlksnon  29924  wspthsnon  29925  clwwlknonmpo  30164  vsfval  30708  dipfval  30777  idlsrgmulr  33588  smatfval  33952  lmatval  33970  qqhval  34129  dya2iocuni  34440  sxbrsigalem5  34445  sitmval  34506  signswplusg  34712  reprval  34767  mclsrcl  35755  mclsval  35757  ldualfvs  39396  paddfval  40057  tgrpopr  41007  erngfplus  41062  erngfmul  41065  erngfplus-rN  41070  erngfmul-rN  41073  dvafvadd  41274  dvafvsca  41276  dvaabl  41284  dvhfvadd  41351  dvhfvsca  41360  djafvalN  41394  djhfval  41657  hlhilip  42208  mendplusgfval  43423  mendmulrfval  43425  mendvscafval  43428  mnringmulrd  44464  mnringmulrcld  44469  hoidmvval  46821  cznrng  48507  cznnring  48508  rngchomfvalALTV  48513  rngccofvalALTV  48516  rngccoALTV  48517  ringchomfvalALTV  48547  ringccofvalALTV  48550  ringccoALTV  48551  rrx2xpreen  48965  lines  48977  spheres  48992  funcf2lem2  49327  upfval  49421  swapfelvv  49508  swapf2fvala  49509  swapf1vala  49511  tposcurf1  49544  diag1f1lem  49551  fucoelvv  49565  fucofn2  49569  fucofvalne  49570  fuco112  49574  fuco111  49575  fuco21  49581  prcofelvv  49625  reldmprcof1  49626  reldmprcof2  49627  prcof1  49633  prcof2a  49634  prcof2  49635  functhinclem1  49689  thincciso  49698  functermc2  49754  incat  49846  setc1onsubc  49847  lanfn  49854  ranfn  49855  lanfval  49858  ranfval  49859