Theorem mpoex 8061

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

Syntax hints:   ∈ wcel 2109  ∀wral 3045  Vcvv 3450   ∈ cmpo 7392

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 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972

This theorem is referenced by:  mptmpoopabbrdOLD  8063  qexALT  12930  ruclem13  16217  vdwapfval  16949  prdsco  17438  imasvsca  17490  homffval  17658  comfffval  17666  comffval  17667  comfffn  17672  comfeq  17674  oppccofval  17684  monfval  17701  sectffval  17719  invffval  17727  cofu1st  17852  cofu2nd  17854  cofucl  17857  natfval  17918  fuccofval  17931  fucco  17934  coafval  18033  setcco  18052  catchomfval  18071  catccofval  18073  catcco  18074  estrcco  18098  xpcval  18145  xpchomfval  18147  xpccofval  18150  xpcco  18151  1stf1  18160  1stf2  18161  2ndf1  18163  2ndf2  18164  1stfcl  18165  2ndfcl  18166  prf1  18168  prf2fval  18169  prfcl  18171  prf1st  18172  prf2nd  18173  evlf2  18186  evlf1  18188  evlfcl  18190  curf1fval  18192  curf11  18194  curf12  18195  curf1cl  18196  curf2  18197  curfcl  18200  hof1fval  18221  hof2fval  18223  hofcl  18227  yonedalem3  18248  efmndplusg  18814  mgmnsgrpex  18865  sgrpnmndex  18866  grpsubfvalALT  18923  mulgfvalALT  19009  symgvalstruct  19334  lsmfval  19575  pj1fval  19631  dvrfval  20318  psrmulr  21858  psrvscafval  21864  evlslem2  21993  mamufval  22286  mvmulfval  22436  isphtpy  24887  pcofval  24917  q1pval  26067  r1pval  26070  mulsproplem9  28034  motplusg  28476  midf  28710  ismidb  28712  ttgval  28809  ebtwntg  28916  ecgrtg  28917  elntg  28918  wwlksnon  29788  wspthsnon  29789  clwwlknonmpo  30025  vsfval  30569  dipfval  30638  idlsrgmulr  33485  smatfval  33792  lmatval  33810  qqhval  33969  dya2iocuni  34281  sxbrsigalem5  34286  sitmval  34347  signswplusg  34553  reprval  34608  mclsrcl  35555  mclsval  35557  ldualfvs  39136  paddfval  39798  tgrpopr  40748  erngfplus  40803  erngfmul  40806  erngfplus-rN  40811  erngfmul-rN  40814  dvafvadd  41015  dvafvsca  41017  dvaabl  41025  dvhfvadd  41092  dvhfvsca  41101  djafvalN  41135  djhfval  41398  hlhilip  41949  mendplusgfval  43177  mendmulrfval  43179  mendvscafval  43182  mnringmulrd  44219  mnringmulrcld  44224  hoidmvval  46582  cznrng  48253  cznnring  48254  rngchomfvalALTV  48259  rngccofvalALTV  48262  rngccoALTV  48263  ringchomfvalALTV  48293  ringccofvalALTV  48296  ringccoALTV  48297  rrx2xpreen  48712  lines  48724  spheres  48739  funcf2lem2  49075  upfval  49169  swapfelvv  49256  swapf2fvala  49257  swapf1vala  49259  tposcurf1  49292  diag1f1lem  49299  fucoelvv  49313  fucofn2  49317  fucofvalne  49318  fuco112  49322  fuco111  49323  fuco21  49329  prcofelvv  49373  reldmprcof1  49374  reldmprcof2  49375  prcof1  49381  prcof2a  49382  prcof2  49383  functhinclem1  49437  thincciso  49446  functermc2  49502  incat  49594  setc1onsubc  49595  lanfn  49602  ranfn  49603  lanfval  49606  ranfval  49607