Theorem mpoex 8120

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

Syntax hints:   ∈ wcel 2108  ∀wral 3067  Vcvv 3488   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031

This theorem is referenced by:  mptmpoopabbrdOLD  8122  qexALT  13029  ruclem13  16290  vdwapfval  17018  prdsco  17528  imasvsca  17580  homffval  17748  comfffval  17756  comffval  17757  comfffn  17762  comfeq  17764  oppccofval  17775  monfval  17793  sectffval  17811  invffval  17819  cofu1st  17947  cofu2nd  17949  cofucl  17952  natfval  18014  fuccofval  18028  fucco  18032  coafval  18131  setcco  18150  catchomfval  18169  catccofval  18171  catcco  18172  estrcco  18198  xpcval  18246  xpchomfval  18248  xpccofval  18251  xpcco  18252  1stf1  18261  1stf2  18262  2ndf1  18264  2ndf2  18265  1stfcl  18266  2ndfcl  18267  prf1  18269  prf2fval  18270  prfcl  18272  prf1st  18273  prf2nd  18274  evlf2  18288  evlf1  18290  evlfcl  18292  curf1fval  18294  curf11  18296  curf12  18297  curf1cl  18298  curf2  18299  curfcl  18302  hof1fval  18323  hof2fval  18325  hofcl  18329  yonedalem3  18350  efmndplusg  18915  mgmnsgrpex  18966  sgrpnmndex  18967  grpsubfvalALT  19024  mulgfvalALT  19110  symgvalstruct  19438  symgvalstructOLD  19439  lsmfval  19680  pj1fval  19736  dvrfval  20428  psrmulr  21985  psrvscafval  21991  evlslem2  22126  mamufval  22417  mvmulfval  22569  isphtpy  25032  pcofval  25062  q1pval  26214  r1pval  26217  mulsproplem9  28168  motplusg  28568  midf  28802  ismidb  28804  ttgval  28901  ttgvalOLD  28902  ebtwntg  29015  ecgrtg  29016  elntg  29017  wwlksnon  29884  wspthsnon  29885  clwwlknonmpo  30121  vsfval  30665  dipfval  30734  idlsrgmulr  33500  smatfval  33741  lmatval  33759  qqhval  33920  dya2iocuni  34248  sxbrsigalem5  34253  sitmval  34314  signswplusg  34532  reprval  34587  mclsrcl  35529  mclsval  35531  ldualfvs  39092  paddfval  39754  tgrpopr  40704  erngfplus  40759  erngfmul  40762  erngfplus-rN  40767  erngfmul-rN  40770  dvafvadd  40971  dvafvsca  40973  dvaabl  40981  dvhfvadd  41048  dvhfvsca  41057  djafvalN  41091  djhfval  41354  hlhilip  41909  mendplusgfval  43142  mendmulrfval  43144  mendvscafval  43147  mnringmulrd  44190  mnringmulrcld  44197  hoidmvval  46498  cznrng  47984  cznnring  47985  rngchomfvalALTV  47990  rngccofvalALTV  47993  rngccoALTV  47994  ringchomfvalALTV  48024  ringccofvalALTV  48027  ringccoALTV  48028  rrx2xpreen  48453  lines  48465  spheres  48480  functhinclem1  48708  thincciso  48716