Theorem mpoexga 8021

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 2736	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
2	1	mpoexg 8020	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3440   ∈ cmpo 7360

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934

This theorem is referenced by:  el2mpocsbcl  8027  bropopvvv  8032  bropfvvvv  8034  prdsip  17381  imasds  17434  isofn  17699  setchomfval  18003  setccofval  18006  estrchomfval  18049  estrccofval  18052  lsmvalx  19568  dfrngc2  20561  funcrngcsetc  20573  dfringc2  20590  funcringcsetc  20607  mamuval  22337  mamudm  22339  marrepfval  22504  marrepval0  22505  marrepval  22506  marepvfval  22509  marepvval  22511  submaval0  22524  submaval  22525  maduval  22582  minmar1val0  22591  minmar1val  22592  mat2pmatval  22668  mat2pmatf  22672  m2cpmf  22686  cpm2mval  22694  decpmatval0  22708  decpmatmul  22716  pmatcollpw2lem  22721  pmatcollpw3lem  22727  mply1topmatval  22748  mp2pm2mplem1  22750  xkoptsub  23598  precsexlem11  28213  grpodivfval  30609  pstmval  34052  sxsigon  34349  cndprobval  34590  lmod1lem1  48743  lmod1lem2  48744  lmod1lem3  48745  lmod1lem4  48746  lmod1lem5  48747  2arymaptfv  48907  2arymaptfo  48910  invfn  49285