Theorem mpoex 8077

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

Syntax hints:   ∈ wcel 2143  ∀wral 3079  Vcvv 3455   ∈ cmpo 7414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-oprab 7416  df-mpo 7417  df-1st 7987  df-2nd 7988

This theorem is referenced by:  qexALT  12989  ruclem13  16299  vdwapfval  17032  prdsco  17522  imasvsca  17575  homffval  17747  comfffval  17755  comffval  17756  comfffn  17761  comfeq  17763  oppccofval  17773  monfval  17790  sectffval  17808  invffval  17816  cofu1st  17941  cofu2nd  17943  cofucl  17946  natfval  18007  fuccofval  18020  fucco  18023  coafval  18122  setcco  18141  catchomfval  18160  catccofval  18162  catcco  18163  estrcco  18187  xpcval  18234  xpchomfval  18236  xpccofval  18239  xpcco  18240  1stf1  18249  1stf2  18250  2ndf1  18252  2ndf2  18253  1stfcl  18254  2ndfcl  18255  prf1  18257  prf2fval  18258  prfcl  18260  prf1st  18261  prf2nd  18262  evlf2  18275  evlf1  18277  evlfcl  18279  curf1fval  18281  curf11  18283  curf12  18284  curf1cl  18285  curf2  18286  curfcl  18289  hof1fval  18310  hof2fval  18312  hofcl  18316  yonedalem3  18337  efmndplusg  18940  mgmnsgrpex  18994  sgrpnmndex  18995  grpsubfvalALT  19052  mulgfvalALT  19137  symgvalstruct  19468  lsmfval  19709  pj1fval  19765  dvrfval  20485  psrmulr  22073  psrvscafval  22079  evlslem2  22211  mamufval  22530  mvmulfval  22680  isphtpy  25121  pcofval  25150  q1pval  26293  r1pval  26296  mulsproplem9  28298  motplusg  28792  midf  29066  ismidb  29068  ttgval  29205  ebtwntg  29313  ecgrtg  29314  elntg  29315  wwlksnon  30181  wspthsnon  30182  clwwlknonmpo  30421  vsfval  30966  dipfval  31035  idlsrgmulr  33778  smatfval  34166  lmatval  34184  qqhval  34343  dya2iocuni  34654  sxbrsigalem5  34659  sitmval  34720  signswplusg  34923  reprval  34978  mclsrcl  36034  mclsval  36036  ldualfvs  39891  paddfval  40552  tgrpopr  41502  erngfplus  41557  erngfmul  41560  erngfplus-rN  41565  erngfmul-rN  41568  dvafvadd  41769  dvafvsca  41771  dvaabl  41779  dvhfvadd  41846  dvhfvsca  41855  djafvalN  41889  djhfval  42152  hlhilip  42703  mendplusgfval  43891  mendmulrfval  43893  mendvscafval  43896  mnringmulrd  44930  mnringmulrcld  44935  hoidmvval  47274  cznrng  49009  cznnring  49010  rngchomfvalALTV  49015  rngccofvalALTV  49018  rngccoALTV  49019  ringchomfvalALTV  49049  ringccofvalALTV  49052  ringccoALTV  49053  rrx2xpreen  49482  lines  49494  spheres  49509  funcf2lem2  49843  upfval  49937  swapfelvv  50024  swapf2fvala  50025  swapf1vala  50027  tposcurf1  50060  diag1f1lem  50067  fucoelvv  50081  fucofn2  50085  fucofvalne  50086  fuco112  50090  fuco111  50091  fuco21  50097  prcofelvv  50141  reldmprcof1  50142  reldmprcof2  50143  prcof1  50149  prcof2a  50150  prcof2  50151  functhinclem1  50205  thincciso  50214  functermc2  50270  incat  50362  setc1onsubc  50363  lanfn  50370  ranfn  50371  lanfval  50374  ranfval  50375