Theorem mpoex 7640

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

Syntax hints:   ∈ wcel 2083  ∀wral 3107  Vcvv 3440   ∈ cmpo 7025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-oprab 7027  df-mpo 7028  df-1st 7552  df-2nd 7553

This theorem is referenced by:  qexALT  12217  ruclem13  15432  vdwapfval  16140  prdsco  16574  imasvsca  16626  homffval  16793  comfffval  16801  comffval  16802  comfffn  16807  comfeq  16809  oppccofval  16819  monfval  16835  sectffval  16853  invffval  16861  cofu1st  16986  cofu2nd  16988  cofucl  16991  natfval  17049  fuccofval  17062  fucco  17065  coafval  17157  setcco  17176  catchomfval  17191  catccofval  17193  catcco  17194  estrcco  17213  xpcval  17260  xpchomfval  17262  xpccofval  17265  xpcco  17266  1stf1  17275  1stf2  17276  2ndf1  17278  2ndf2  17279  1stfcl  17280  2ndfcl  17281  prf1  17283  prf2fval  17284  prfcl  17286  prf1st  17287  prf2nd  17288  evlf2  17301  evlf1  17303  evlfcl  17305  curf1fval  17307  curf11  17309  curf12  17310  curf1cl  17311  curf2  17312  curfcl  17315  hof1fval  17336  hof2fval  17338  hofcl  17342  yonedalem3  17363  mgmnsgrpex  17861  sgrpnmndex  17862  grpsubfvalALT  17909  mulgfvalALT  17988  symgplusg  18252  lsmfval  18497  pj1fval  18551  dvrfval  19128  psrmulr  19856  psrvscafval  19862  evlslem2  19983  mamufval  20682  mvmulfval  20839  isphtpy  23272  pcofval  23301  q1pval  24434  r1pval  24437  motplusg  26014  midf  26248  ismidb  26250  ttgval  26348  ebtwntg  26455  ecgrtg  26456  elntg  26457  wwlksnon  27315  wspthsnon  27316  clwwlknonmpo  27554  vsfval  28097  dipfval  28166  smatfval  30671  lmatval  30689  qqhval  30828  dya2iocuni  31154  sxbrsigalem5  31159  sitmval  31220  signswplusg  31438  reprval  31494  mclsrcl  32418  mclsval  32420  ldualfvs  35824  paddfval  36485  tgrpopr  37435  erngfplus  37490  erngfmul  37493  erngfplus-rN  37498  erngfmul-rN  37501  dvafvadd  37702  dvafvsca  37704  dvaabl  37712  dvhfvadd  37779  dvhfvsca  37788  djafvalN  37822  djhfval  38085  hlhilip  38636  mendplusgfval  39291  mendmulrfval  39293  mendvscafval  39296  hoidmvval  42423  cznrng  43726  cznnring  43727  rngchomfvalALTV  43755  rngccofvalALTV  43758  rngccoALTV  43759  ringchomfvalALTV  43818  ringccofvalALTV  43821  ringccoALTV  43822  rrx2xpreen  44209  lines  44221  spheres  44236