Theorem mpoex 8020

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

Syntax hints:   ∈ wcel 2113  ∀wral 3049  Vcvv 3438   ∈ cmpo 7357

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 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-oprab 7359  df-mpo 7360  df-1st 7930  df-2nd 7931

This theorem is referenced by:  mptmpoopabbrdOLD  8022  qexALT  12872  ruclem13  16161  vdwapfval  16893  prdsco  17382  imasvsca  17434  homffval  17606  comfffval  17614  comffval  17615  comfffn  17620  comfeq  17622  oppccofval  17632  monfval  17649  sectffval  17667  invffval  17675  cofu1st  17800  cofu2nd  17802  cofucl  17805  natfval  17866  fuccofval  17879  fucco  17882  coafval  17981  setcco  18000  catchomfval  18019  catccofval  18021  catcco  18022  estrcco  18046  xpcval  18093  xpchomfval  18095  xpccofval  18098  xpcco  18099  1stf1  18108  1stf2  18109  2ndf1  18111  2ndf2  18112  1stfcl  18113  2ndfcl  18114  prf1  18116  prf2fval  18117  prfcl  18119  prf1st  18120  prf2nd  18121  evlf2  18134  evlf1  18136  evlfcl  18138  curf1fval  18140  curf11  18142  curf12  18143  curf1cl  18144  curf2  18145  curfcl  18148  hof1fval  18169  hof2fval  18171  hofcl  18175  yonedalem3  18196  efmndplusg  18798  mgmnsgrpex  18849  sgrpnmndex  18850  grpsubfvalALT  18907  mulgfvalALT  18993  symgvalstruct  19319  lsmfval  19560  pj1fval  19616  dvrfval  20330  psrmulr  21889  psrvscafval  21895  evlslem2  22024  mamufval  22317  mvmulfval  22467  isphtpy  24917  pcofval  24947  q1pval  26097  r1pval  26100  mulsproplem9  28073  motplusg  28530  midf  28764  ismidb  28766  ttgval  28863  ebtwntg  28971  ecgrtg  28972  elntg  28973  wwlksnon  29840  wspthsnon  29841  clwwlknonmpo  30080  vsfval  30624  dipfval  30693  idlsrgmulr  33483  smatfval  33819  lmatval  33837  qqhval  33996  dya2iocuni  34307  sxbrsigalem5  34312  sitmval  34373  signswplusg  34579  reprval  34634  mclsrcl  35616  mclsval  35618  ldualfvs  39245  paddfval  39906  tgrpopr  40856  erngfplus  40911  erngfmul  40914  erngfplus-rN  40919  erngfmul-rN  40922  dvafvadd  41123  dvafvsca  41125  dvaabl  41133  dvhfvadd  41200  dvhfvsca  41209  djafvalN  41243  djhfval  41506  hlhilip  42057  mendplusgfval  43288  mendmulrfval  43290  mendvscafval  43293  mnringmulrd  44330  mnringmulrcld  44335  hoidmvval  46689  cznrng  48375  cznnring  48376  rngchomfvalALTV  48381  rngccofvalALTV  48384  rngccoALTV  48385  ringchomfvalALTV  48415  ringccofvalALTV  48418  ringccoALTV  48419  rrx2xpreen  48834  lines  48846  spheres  48861  funcf2lem2  49197  upfval  49291  swapfelvv  49378  swapf2fvala  49379  swapf1vala  49381  tposcurf1  49414  diag1f1lem  49421  fucoelvv  49435  fucofn2  49439  fucofvalne  49440  fuco112  49444  fuco111  49445  fuco21  49451  prcofelvv  49495  reldmprcof1  49496  reldmprcof2  49497  prcof1  49503  prcof2a  49504  prcof2  49505  functhinclem1  49559  thincciso  49568  functermc2  49624  incat  49716  setc1onsubc  49717  lanfn  49724  ranfn  49725  lanfval  49728  ranfval  49729