Theorem mpoex 8037

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044  Vcvv 3444   ∈ cmpo 7371

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 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948

This theorem is referenced by:  mptmpoopabbrdOLD  8039  qexALT  12899  ruclem13  16186  vdwapfval  16918  prdsco  17407  imasvsca  17459  homffval  17627  comfffval  17635  comffval  17636  comfffn  17641  comfeq  17643  oppccofval  17653  monfval  17670  sectffval  17688  invffval  17696  cofu1st  17821  cofu2nd  17823  cofucl  17826  natfval  17887  fuccofval  17900  fucco  17903  coafval  18002  setcco  18021  catchomfval  18040  catccofval  18042  catcco  18043  estrcco  18067  xpcval  18114  xpchomfval  18116  xpccofval  18119  xpcco  18120  1stf1  18129  1stf2  18130  2ndf1  18132  2ndf2  18133  1stfcl  18134  2ndfcl  18135  prf1  18137  prf2fval  18138  prfcl  18140  prf1st  18141  prf2nd  18142  evlf2  18155  evlf1  18157  evlfcl  18159  curf1fval  18161  curf11  18163  curf12  18164  curf1cl  18165  curf2  18166  curfcl  18169  hof1fval  18190  hof2fval  18192  hofcl  18196  yonedalem3  18217  efmndplusg  18783  mgmnsgrpex  18834  sgrpnmndex  18835  grpsubfvalALT  18892  mulgfvalALT  18978  symgvalstruct  19303  lsmfval  19544  pj1fval  19600  dvrfval  20287  psrmulr  21827  psrvscafval  21833  evlslem2  21962  mamufval  22255  mvmulfval  22405  isphtpy  24856  pcofval  24886  q1pval  26036  r1pval  26039  mulsproplem9  28003  motplusg  28445  midf  28679  ismidb  28681  ttgval  28778  ebtwntg  28885  ecgrtg  28886  elntg  28887  wwlksnon  29754  wspthsnon  29755  clwwlknonmpo  29991  vsfval  30535  dipfval  30604  idlsrgmulr  33451  smatfval  33758  lmatval  33776  qqhval  33935  dya2iocuni  34247  sxbrsigalem5  34252  sitmval  34313  signswplusg  34519  reprval  34574  mclsrcl  35521  mclsval  35523  ldualfvs  39102  paddfval  39764  tgrpopr  40714  erngfplus  40769  erngfmul  40772  erngfplus-rN  40777  erngfmul-rN  40780  dvafvadd  40981  dvafvsca  40983  dvaabl  40991  dvhfvadd  41058  dvhfvsca  41067  djafvalN  41101  djhfval  41364  hlhilip  41915  mendplusgfval  43143  mendmulrfval  43145  mendvscafval  43148  mnringmulrd  44185  mnringmulrcld  44190  hoidmvval  46548  cznrng  48222  cznnring  48223  rngchomfvalALTV  48228  rngccofvalALTV  48231  rngccoALTV  48232  ringchomfvalALTV  48262  ringccofvalALTV  48265  ringccoALTV  48266  rrx2xpreen  48681  lines  48693  spheres  48708  funcf2lem2  49044  upfval  49138  swapfelvv  49225  swapf2fvala  49226  swapf1vala  49228  tposcurf1  49261  diag1f1lem  49268  fucoelvv  49282  fucofn2  49286  fucofvalne  49287  fuco112  49291  fuco111  49292  fuco21  49298  prcofelvv  49342  reldmprcof1  49343  reldmprcof2  49344  prcof1  49350  prcof2a  49351  prcof2  49352  functhinclem1  49406  thincciso  49415  functermc2  49471  incat  49563  setc1onsubc  49564  lanfn  49571  ranfn  49572  lanfval  49575  ranfval  49576