Theorem mpoex 8127

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

This proof depends on syntax axioms:   ∈ wcel 2147  ∀wral 3080  Vcvv 3454   ∈ cmpo 7453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036

This theorem is used by:  qexALT  13131  ruclem13  16454  vdwapfval  17193  prdsco  17689  imasvsca  17742  homffval  17914  comfffval  17922  comffval  17923  comfffn  17928  comfeq  17930  oppccofval  17940  monfval  17957  sectffval  17975  invffval  17983  cofu1st  18108  cofu2nd  18110  cofucl  18113  natfval  18174  fuccofval  18187  fucco  18190  coafval  18289  setcco  18308  catchomfval  18327  catccofval  18329  catcco  18330  estrcco  18354  xpcval  18401  xpchomfval  18403  xpccofval  18406  xpcco  18407  1stf1  18416  1stf2  18417  2ndf1  18419  2ndf2  18420  1stfcl  18421  2ndfcl  18422  prf1  18424  prf2fval  18425  prfcl  18427  prf1st  18428  prf2nd  18429  evlf2  18442  evlf1  18444  evlfcl  18446  curf1fval  18448  curf11  18450  curf12  18451  curf1cl  18452  curf2  18453  curfcl  18456  hof1fval  18477  hof2fval  18479  hofcl  18483  yonedalem3  18504  efmndplusg  19126  mgmnsgrpex  19180  sgrpnmndex  19181  grpsubfvalALT  19245  mulgfvalALT  19330  symgvalstruct  19662  lsmfval  19903  pj1fval  19959  dvrfval  20683  psrmulr  22305  psrvscafval  22311  evlslem2  22443  mamufval  22762  mvmulfval  22912  isphtpy  25357  pcofval  25386  q1pval  26528  r1pval  26531  mulsproplem9  28567  motplusg  29062  midf  29338  ismidb  29340  angmgmlem  29452  ttgval  29509  ebtwntg  29617  ecgrtg  29618  elntg  29619  wwlksnon  30497  wspthsnon  30498  clwwlknonmpo  30737  vsfval  31292  dipfval  31361  idlsrgmulr  34143  smatfval  34538  lmatval  34556  qqhval  34715  dya2iocuni  35026  sxbrsigalem5  35031  sitmval  35092  signswplusg  35295  reprval  35350  mclsrcl  36534  mclsval  36536  ldualfvs  40459  paddfval  41120  tgrpopr  42070  erngfplus  42125  erngfmul  42128  erngfplus-rN  42133  erngfmul-rN  42136  dvafvadd  42337  dvafvsca  42339  dvaabl  42347  dvhfvadd  42414  dvhfvsca  42423  djafvalN  42457  djhfval  42720  hlhilip  43271  mendplusgfval  44444  mendmulrfval  44446  mendvscafval  44449  mnringmulrd  45482  mnringmulrcld  45487  hoidmvval  47860  cznrng  49631  cznnring  49632  rngchomfvalALTV  49637  rngccofvalALTV  49640  rngccoALTV  49641  ringchomfvalALTV  49671  ringccofvalALTV  49674  ringccoALTV  49675  rrx2xpreen  50163  lines  50175  spheres  50189  funcf2lem2  50527  upfval  50623  swapfelvv  50716  swapf2fvala  50717  swapf1vala  50719  tposcurf1  50752  diag1f1lem  50759  fucoelvv  50773  fucofn2  50777  fucofvalne  50778  fuco112  50782  fuco111  50783  fuco21  50789  postcof1st  50829  postcof2nd  50830  prcofelvv  50846  reldmprcof1  50847  reldmprcof2  50848  prcof1  50854  prcof2a  50855  prcof2  50856  functhinclem1  50910  thincciso  50919  functermc2  50975  incat  51070  setc1onsubc  51071  parcatid2  51094  parcatid  51095  par2str  51100  parmapfunc2  51105  fuconuniqlem  51112  fuconuniqvalslem  51114  lanfn  51123  ranfn  51124  lanfval  51127  ranfval  51128  crosspdot0lem  51391