Theorem mpoex 8021

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044  Vcvv 3438   ∈ cmpo 7355

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 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

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 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-oprab 7357  df-mpo 7358  df-1st 7931  df-2nd 7932

This theorem is referenced by:  mptmpoopabbrdOLD  8023  qexALT  12884  ruclem13  16170  vdwapfval  16902  prdsco  17391  imasvsca  17443  homffval  17615  comfffval  17623  comffval  17624  comfffn  17629  comfeq  17631  oppccofval  17641  monfval  17658  sectffval  17676  invffval  17684  cofu1st  17809  cofu2nd  17811  cofucl  17814  natfval  17875  fuccofval  17888  fucco  17891  coafval  17990  setcco  18009  catchomfval  18028  catccofval  18030  catcco  18031  estrcco  18055  xpcval  18102  xpchomfval  18104  xpccofval  18107  xpcco  18108  1stf1  18117  1stf2  18118  2ndf1  18120  2ndf2  18121  1stfcl  18122  2ndfcl  18123  prf1  18125  prf2fval  18126  prfcl  18128  prf1st  18129  prf2nd  18130  evlf2  18143  evlf1  18145  evlfcl  18147  curf1fval  18149  curf11  18151  curf12  18152  curf1cl  18153  curf2  18154  curfcl  18157  hof1fval  18178  hof2fval  18180  hofcl  18184  yonedalem3  18205  efmndplusg  18773  mgmnsgrpex  18824  sgrpnmndex  18825  grpsubfvalALT  18882  mulgfvalALT  18968  symgvalstruct  19295  lsmfval  19536  pj1fval  19592  dvrfval  20306  psrmulr  21868  psrvscafval  21874  evlslem2  22003  mamufval  22296  mvmulfval  22446  isphtpy  24897  pcofval  24927  q1pval  26077  r1pval  26080  mulsproplem9  28051  motplusg  28506  midf  28740  ismidb  28742  ttgval  28839  ebtwntg  28946  ecgrtg  28947  elntg  28948  wwlksnon  29815  wspthsnon  29816  clwwlknonmpo  30052  vsfval  30596  dipfval  30665  idlsrgmulr  33463  smatfval  33781  lmatval  33799  qqhval  33958  dya2iocuni  34270  sxbrsigalem5  34275  sitmval  34336  signswplusg  34542  reprval  34597  mclsrcl  35553  mclsval  35555  ldualfvs  39134  paddfval  39796  tgrpopr  40746  erngfplus  40801  erngfmul  40804  erngfplus-rN  40809  erngfmul-rN  40812  dvafvadd  41013  dvafvsca  41015  dvaabl  41023  dvhfvadd  41090  dvhfvsca  41099  djafvalN  41133  djhfval  41396  hlhilip  41947  mendplusgfval  43174  mendmulrfval  43176  mendvscafval  43179  mnringmulrd  44216  mnringmulrcld  44221  hoidmvval  46578  cznrng  48265  cznnring  48266  rngchomfvalALTV  48271  rngccofvalALTV  48274  rngccoALTV  48275  ringchomfvalALTV  48305  ringccofvalALTV  48308  ringccoALTV  48309  rrx2xpreen  48724  lines  48736  spheres  48751  funcf2lem2  49087  upfval  49181  swapfelvv  49268  swapf2fvala  49269  swapf1vala  49271  tposcurf1  49304  diag1f1lem  49311  fucoelvv  49325  fucofn2  49329  fucofvalne  49330  fuco112  49334  fuco111  49335  fuco21  49341  prcofelvv  49385  reldmprcof1  49386  reldmprcof2  49387  prcof1  49393  prcof2a  49394  prcof2  49395  functhinclem1  49449  thincciso  49458  functermc2  49514  incat  49606  setc1onsubc  49607  lanfn  49614  ranfn  49615  lanfval  49618  ranfval  49619