Theorem mpoex 7777

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

Syntax hints:   ∈ wcel 2114  ∀wral 3138  Vcvv 3494   ∈ cmpo 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690

This theorem is referenced by:  qexALT  12364  ruclem13  15595  vdwapfval  16307  prdsco  16741  imasvsca  16793  homffval  16960  comfffval  16968  comffval  16969  comfffn  16974  comfeq  16976  oppccofval  16986  monfval  17002  sectffval  17020  invffval  17028  cofu1st  17153  cofu2nd  17155  cofucl  17158  natfval  17216  fuccofval  17229  fucco  17232  coafval  17324  setcco  17343  catchomfval  17358  catccofval  17360  catcco  17361  estrcco  17380  xpcval  17427  xpchomfval  17429  xpccofval  17432  xpcco  17433  1stf1  17442  1stf2  17443  2ndf1  17445  2ndf2  17446  1stfcl  17447  2ndfcl  17448  prf1  17450  prf2fval  17451  prfcl  17453  prf1st  17454  prf2nd  17455  evlf2  17468  evlf1  17470  evlfcl  17472  curf1fval  17474  curf11  17476  curf12  17477  curf1cl  17478  curf2  17479  curfcl  17482  hof1fval  17503  hof2fval  17505  hofcl  17509  yonedalem3  17530  efmndplusg  18045  mgmnsgrpex  18096  sgrpnmndex  18097  grpsubfvalALT  18148  mulgfvalALT  18227  symgvalstruct  18525  lsmfval  18763  pj1fval  18820  dvrfval  19434  psrmulr  20164  psrvscafval  20170  evlslem2  20292  mamufval  20996  mvmulfval  21151  isphtpy  23585  pcofval  23614  q1pval  24747  r1pval  24750  motplusg  26328  midf  26562  ismidb  26564  ttgval  26661  ebtwntg  26768  ecgrtg  26769  elntg  26770  wwlksnon  27629  wspthsnon  27630  clwwlknonmpo  27868  vsfval  28410  dipfval  28479  smatfval  31060  lmatval  31078  qqhval  31215  dya2iocuni  31541  sxbrsigalem5  31546  sitmval  31607  signswplusg  31825  reprval  31881  mclsrcl  32808  mclsval  32810  ldualfvs  36287  paddfval  36948  tgrpopr  37898  erngfplus  37953  erngfmul  37956  erngfplus-rN  37961  erngfmul-rN  37964  dvafvadd  38165  dvafvsca  38167  dvaabl  38175  dvhfvadd  38242  dvhfvsca  38251  djafvalN  38285  djhfval  38548  hlhilip  39099  mendplusgfval  39834  mendmulrfval  39836  mendvscafval  39839  hoidmvval  42908  cznrng  44275  cznnring  44276  rngchomfvalALTV  44304  rngccofvalALTV  44307  rngccoALTV  44308  ringchomfvalALTV  44367  ringccofvalALTV  44370  ringccoALTV  44371  rrx2xpreen  44755  lines  44767  spheres  44782