Theorem mpoex 8033

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

Syntax hints:   ∈ wcel 2114  ∀wral 3052  Vcvv 3442   ∈ cmpo 7370

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 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944

This theorem is referenced by:  mptmpoopabbrdOLD  8035  qexALT  12889  ruclem13  16179  vdwapfval  16911  prdsco  17400  imasvsca  17453  homffval  17625  comfffval  17633  comffval  17634  comfffn  17639  comfeq  17641  oppccofval  17651  monfval  17668  sectffval  17686  invffval  17694  cofu1st  17819  cofu2nd  17821  cofucl  17824  natfval  17885  fuccofval  17898  fucco  17901  coafval  18000  setcco  18019  catchomfval  18038  catccofval  18040  catcco  18041  estrcco  18065  xpcval  18112  xpchomfval  18114  xpccofval  18117  xpcco  18118  1stf1  18127  1stf2  18128  2ndf1  18130  2ndf2  18131  1stfcl  18132  2ndfcl  18133  prf1  18135  prf2fval  18136  prfcl  18138  prf1st  18139  prf2nd  18140  evlf2  18153  evlf1  18155  evlfcl  18157  curf1fval  18159  curf11  18161  curf12  18162  curf1cl  18163  curf2  18164  curfcl  18167  hof1fval  18188  hof2fval  18190  hofcl  18194  yonedalem3  18215  efmndplusg  18817  mgmnsgrpex  18868  sgrpnmndex  18869  grpsubfvalALT  18926  mulgfvalALT  19012  symgvalstruct  19338  lsmfval  19579  pj1fval  19635  dvrfval  20350  psrmulr  21910  psrvscafval  21916  evlslem2  22046  mamufval  22348  mvmulfval  22498  isphtpy  24948  pcofval  24978  q1pval  26128  r1pval  26131  mulsproplem9  28132  motplusg  28626  midf  28860  ismidb  28862  ttgval  28959  ebtwntg  29067  ecgrtg  29068  elntg  29069  wwlksnon  29936  wspthsnon  29937  clwwlknonmpo  30176  vsfval  30720  dipfval  30789  idlsrgmulr  33599  smatfval  33972  lmatval  33990  qqhval  34149  dya2iocuni  34460  sxbrsigalem5  34465  sitmval  34526  signswplusg  34732  reprval  34787  mclsrcl  35774  mclsval  35776  ldualfvs  39509  paddfval  40170  tgrpopr  41120  erngfplus  41175  erngfmul  41178  erngfplus-rN  41183  erngfmul-rN  41186  dvafvadd  41387  dvafvsca  41389  dvaabl  41397  dvhfvadd  41464  dvhfvsca  41473  djafvalN  41507  djhfval  41770  hlhilip  42321  mendplusgfval  43535  mendmulrfval  43537  mendvscafval  43540  mnringmulrd  44576  mnringmulrcld  44581  hoidmvval  46932  cznrng  48618  cznnring  48619  rngchomfvalALTV  48624  rngccofvalALTV  48627  rngccoALTV  48628  ringchomfvalALTV  48658  ringccofvalALTV  48661  ringccoALTV  48662  rrx2xpreen  49076  lines  49088  spheres  49103  funcf2lem2  49438  upfval  49532  swapfelvv  49619  swapf2fvala  49620  swapf1vala  49622  tposcurf1  49655  diag1f1lem  49662  fucoelvv  49676  fucofn2  49680  fucofvalne  49681  fuco112  49685  fuco111  49686  fuco21  49692  prcofelvv  49736  reldmprcof1  49737  reldmprcof2  49738  prcof1  49744  prcof2a  49745  prcof2  49746  functhinclem1  49800  thincciso  49809  functermc2  49865  incat  49957  setc1onsubc  49958  lanfn  49965  ranfn  49966  lanfval  49969  ranfval  49970