Theorem mpoex 8032

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

Syntax hints:   ∈ wcel 2114  ∀wral 3051  Vcvv 3429   ∈ cmpo 7369

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  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 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943

This theorem is referenced by:  qexALT  12914  ruclem13  16209  vdwapfval  16942  prdsco  17431  imasvsca  17484  homffval  17656  comfffval  17664  comffval  17665  comfffn  17670  comfeq  17672  oppccofval  17682  monfval  17699  sectffval  17717  invffval  17725  cofu1st  17850  cofu2nd  17852  cofucl  17855  natfval  17916  fuccofval  17929  fucco  17932  coafval  18031  setcco  18050  catchomfval  18069  catccofval  18071  catcco  18072  estrcco  18096  xpcval  18143  xpchomfval  18145  xpccofval  18148  xpcco  18149  1stf1  18158  1stf2  18159  2ndf1  18161  2ndf2  18162  1stfcl  18163  2ndfcl  18164  prf1  18166  prf2fval  18167  prfcl  18169  prf1st  18170  prf2nd  18171  evlf2  18184  evlf1  18186  evlfcl  18188  curf1fval  18190  curf11  18192  curf12  18193  curf1cl  18194  curf2  18195  curfcl  18198  hof1fval  18219  hof2fval  18221  hofcl  18225  yonedalem3  18246  efmndplusg  18848  mgmnsgrpex  18902  sgrpnmndex  18903  grpsubfvalALT  18960  mulgfvalALT  19046  symgvalstruct  19372  lsmfval  19613  pj1fval  19669  dvrfval  20382  psrmulr  21921  psrvscafval  21927  evlslem2  22057  mamufval  22357  mvmulfval  22507  isphtpy  24948  pcofval  24977  q1pval  26120  r1pval  26123  mulsproplem9  28116  motplusg  28610  midf  28844  ismidb  28846  ttgval  28943  ebtwntg  29051  ecgrtg  29052  elntg  29053  wwlksnon  29919  wspthsnon  29920  clwwlknonmpo  30159  vsfval  30704  dipfval  30773  idlsrgmulr  33567  smatfval  33939  lmatval  33957  qqhval  34116  dya2iocuni  34427  sxbrsigalem5  34432  sitmval  34493  signswplusg  34699  reprval  34754  mclsrcl  35743  mclsval  35745  ldualfvs  39582  paddfval  40243  tgrpopr  41193  erngfplus  41248  erngfmul  41251  erngfplus-rN  41256  erngfmul-rN  41259  dvafvadd  41460  dvafvsca  41462  dvaabl  41470  dvhfvadd  41537  dvhfvsca  41546  djafvalN  41580  djhfval  41843  hlhilip  42394  mendplusgfval  43609  mendmulrfval  43611  mendvscafval  43614  mnringmulrd  44650  mnringmulrcld  44655  hoidmvval  47005  cznrng  48737  cznnring  48738  rngchomfvalALTV  48743  rngccofvalALTV  48746  rngccoALTV  48747  ringchomfvalALTV  48777  ringccofvalALTV  48780  ringccoALTV  48781  rrx2xpreen  49195  lines  49207  spheres  49222  funcf2lem2  49557  upfval  49651  swapfelvv  49738  swapf2fvala  49739  swapf1vala  49741  tposcurf1  49774  diag1f1lem  49781  fucoelvv  49795  fucofn2  49799  fucofvalne  49800  fuco112  49804  fuco111  49805  fuco21  49811  prcofelvv  49855  reldmprcof1  49856  reldmprcof2  49857  prcof1  49863  prcof2a  49864  prcof2  49865  functhinclem1  49919  thincciso  49928  functermc2  49984  incat  50076  setc1onsubc  50077  lanfn  50084  ranfn  50085  lanfval  50088  ranfval  50089