Theorem mpoexga 8101

Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011.)

Assertion

Ref	Expression
mpoexga	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem mpoexga

Step	Hyp	Ref	Expression
1		eqid 2735	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
2	1	mpoexg 8100	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  Vcvv 3478   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014

This theorem is referenced by:  mptmpoopabbrdOLDOLD  8107  el2mpocsbcl  8109  bropopvvv  8114  bropfvvvv  8116  prdsip  17508  imasds  17560  isofn  17823  setchomfval  18133  setccofval  18136  estrchomfval  18181  estrccofval  18184  lsmvalx  19672  dfrngc2  20645  funcrngcsetc  20657  dfringc2  20674  funcringcsetc  20691  mamuval  22413  mamudm  22415  marrepfval  22582  marrepval0  22583  marrepval  22584  marepvfval  22587  marepvval  22589  submaval0  22602  submaval  22603  maduval  22660  minmar1val0  22669  minmar1val  22670  mat2pmatval  22746  mat2pmatf  22750  m2cpmf  22764  cpm2mval  22772  decpmatval0  22786  decpmatmul  22794  pmatcollpw2lem  22799  pmatcollpw3lem  22805  mply1topmatval  22826  mp2pm2mplem1  22828  xkoptsub  23678  precsexlem11  28256  grpodivfval  30563  pstmval  33856  sxsigon  34173  cndprobval  34415  lmod1lem1  48333  lmod1lem2  48334  lmod1lem3  48335  lmod1lem4  48336  lmod1lem5  48337  2arymaptfv  48501  2arymaptfo  48504