Theorem mpoex 8078

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

This proof depends on syntax axioms:   ∈ wcel 2145  ∀wral 3076  Vcvv 3450   ∈ cmpo 7415

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-oprab 7417  df-mpo 7418  df-1st 7986  df-2nd 7987

This theorem is used by:  qexALT  13013  ruclem13  16330  vdwapfval  17063  prdsco  17553  imasvsca  17606  homffval  17778  comfffval  17786  comffval  17787  comfffn  17792  comfeq  17794  oppccofval  17804  monfval  17821  sectffval  17839  invffval  17847  cofu1st  17972  cofu2nd  17974  cofucl  17977  natfval  18038  fuccofval  18051  fucco  18054  coafval  18153  setcco  18172  catchomfval  18191  catccofval  18193  catcco  18194  estrcco  18218  xpcval  18265  xpchomfval  18267  xpccofval  18270  xpcco  18271  1stf1  18280  1stf2  18281  2ndf1  18283  2ndf2  18284  1stfcl  18285  2ndfcl  18286  prf1  18288  prf2fval  18289  prfcl  18291  prf1st  18292  prf2nd  18293  evlf2  18306  evlf1  18308  evlfcl  18310  curf1fval  18312  curf11  18314  curf12  18315  curf1cl  18316  curf2  18317  curfcl  18320  hof1fval  18341  hof2fval  18343  hofcl  18347  yonedalem3  18368  efmndplusg  18989  mgmnsgrpex  19043  sgrpnmndex  19044  grpsubfvalALT  19108  mulgfvalALT  19193  symgvalstruct  19524  lsmfval  19765  pj1fval  19821  dvrfval  20543  psrmulr  22157  psrvscafval  22163  evlslem2  22295  mamufval  22614  mvmulfval  22764  isphtpy  25209  pcofval  25238  q1pval  26380  r1pval  26383  mulsproplem9  28389  motplusg  28884  midf  29160  ismidb  29162  angmgmlem  29274  ttgval  29331  ebtwntg  29439  ecgrtg  29440  elntg  29441  wwlksnon  30319  wspthsnon  30320  clwwlknonmpo  30559  vsfval  31114  dipfval  31183  idlsrgmulr  33917  smatfval  34305  lmatval  34323  qqhval  34482  dya2iocuni  34794  sxbrsigalem5  34799  sitmval  34860  signswplusg  35063  reprval  35118  mclsrcl  36140  mclsval  36142  ldualfvs  40009  paddfval  40670  tgrpopr  41620  erngfplus  41675  erngfmul  41678  erngfplus-rN  41683  erngfmul-rN  41686  dvafvadd  41887  dvafvsca  41889  dvaabl  41897  dvhfvadd  41964  dvhfvsca  41973  djafvalN  42007  djhfval  42270  hlhilip  42821  mendplusgfval  44022  mendmulrfval  44024  mendvscafval  44027  mnringmulrd  45061  mnringmulrcld  45066  hoidmvval  47405  cznrng  49176  cznnring  49177  rngchomfvalALTV  49182  rngccofvalALTV  49185  rngccoALTV  49186  ringchomfvalALTV  49216  ringccofvalALTV  49219  ringccoALTV  49220  rrx2xpreen  49649  lines  49661  spheres  49676  funcf2lem2  50008  upfval  50102  swapfelvv  50189  swapf2fvala  50190  swapf1vala  50192  tposcurf1  50225  diag1f1lem  50232  fucoelvv  50246  fucofn2  50250  fucofvalne  50251  fuco112  50255  fuco111  50256  fuco21  50262  prcofelvv  50306  reldmprcof1  50307  reldmprcof2  50308  prcof1  50314  prcof2a  50315  prcof2  50316  functhinclem1  50370  thincciso  50379  functermc2  50435  incat  50527  setc1onsubc  50528  lanfn  50535  ranfn  50536  lanfval  50539  ranfval  50540  crosspdot0lem  50796