Theorem mpoex 8090

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

This proof depends on syntax axioms:   ∈ wcel 2145  ∀wral 3077  Vcvv 3451   ∈ cmpo 7420

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 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-oprab 7422  df-mpo 7423  df-1st 7999  df-2nd 8000

This theorem is used by:  qexALT  13084  ruclem13  16403  vdwapfval  17142  prdsco  17632  imasvsca  17685  homffval  17857  comfffval  17865  comffval  17866  comfffn  17871  comfeq  17873  oppccofval  17883  monfval  17900  sectffval  17918  invffval  17926  cofu1st  18051  cofu2nd  18053  cofucl  18056  natfval  18117  fuccofval  18130  fucco  18133  coafval  18232  setcco  18251  catchomfval  18270  catccofval  18272  catcco  18273  estrcco  18297  xpcval  18344  xpchomfval  18346  xpccofval  18349  xpcco  18350  1stf1  18359  1stf2  18360  2ndf1  18362  2ndf2  18363  1stfcl  18364  2ndfcl  18365  prf1  18367  prf2fval  18368  prfcl  18370  prf1st  18371  prf2nd  18372  evlf2  18385  evlf1  18387  evlfcl  18389  curf1fval  18391  curf11  18393  curf12  18394  curf1cl  18395  curf2  18396  curfcl  18399  hof1fval  18420  hof2fval  18422  hofcl  18426  yonedalem3  18447  efmndplusg  19069  mgmnsgrpex  19123  sgrpnmndex  19124  grpsubfvalALT  19188  mulgfvalALT  19273  symgvalstruct  19604  lsmfval  19845  pj1fval  19901  dvrfval  20625  psrmulr  22243  psrvscafval  22249  evlslem2  22381  mamufval  22700  mvmulfval  22850  isphtpy  25295  pcofval  25324  q1pval  26466  r1pval  26469  mulsproplem9  28503  motplusg  28998  midf  29274  ismidb  29276  angmgmlem  29388  ttgval  29445  ebtwntg  29553  ecgrtg  29554  elntg  29555  wwlksnon  30433  wspthsnon  30434  clwwlknonmpo  30673  vsfval  31228  dipfval  31297  idlsrgmulr  34032  smatfval  34420  lmatval  34438  qqhval  34597  dya2iocuni  34908  sxbrsigalem5  34913  sitmval  34974  signswplusg  35177  reprval  35232  mclsrcl  36305  mclsval  36307  ldualfvs  40173  paddfval  40834  tgrpopr  41784  erngfplus  41839  erngfmul  41842  erngfplus-rN  41847  erngfmul-rN  41850  dvafvadd  42051  dvafvsca  42053  dvaabl  42061  dvhfvadd  42128  dvhfvsca  42137  djafvalN  42171  djhfval  42434  hlhilip  42985  mendplusgfval  44167  mendmulrfval  44169  mendvscafval  44172  mnringmulrd  45206  mnringmulrcld  45211  hoidmvval  47556  cznrng  49327  cznnring  49328  rngchomfvalALTV  49333  rngccofvalALTV  49336  rngccoALTV  49337  ringchomfvalALTV  49367  ringccofvalALTV  49370  ringccoALTV  49371  rrx2xpreen  49800  lines  49812  spheres  49827  funcf2lem2  50159  upfval  50253  swapfelvv  50340  swapf2fvala  50341  swapf1vala  50343  tposcurf1  50376  diag1f1lem  50383  fucoelvv  50397  fucofn2  50401  fucofvalne  50402  fuco112  50406  fuco111  50407  fuco21  50413  prcofelvv  50457  reldmprcof1  50458  reldmprcof2  50459  prcof1  50465  prcof2a  50466  prcof2  50467  functhinclem1  50521  thincciso  50530  functermc2  50586  incat  50678  setc1onsubc  50679  lanfn  50686  ranfn  50687  lanfval  50690  ranfval  50691  crosspdot0lem  50932