Theorem mpoexga 7918

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3432   ∈ cmpo 7277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832

This theorem is referenced by:  mptmpoopabbrdOLD  7923  el2mpocsbcl  7925  bropopvvv  7930  bropfvvvv  7932  prdsip  17172  imasds  17224  isofn  17487  setchomfval  17794  setccofval  17797  estrchomfval  17842  estrccofval  17845  lsmvalx  19244  mamuval  21535  mamudm  21537  marrepfval  21709  marrepval0  21710  marrepval  21711  marepvfval  21714  marepvval  21716  submaval0  21729  submaval  21730  maduval  21787  minmar1val0  21796  minmar1val  21797  mat2pmatval  21873  mat2pmatf  21877  m2cpmf  21891  cpm2mval  21899  decpmatval0  21913  decpmatmul  21921  pmatcollpw2lem  21926  pmatcollpw3lem  21932  mply1topmatval  21953  mp2pm2mplem1  21955  xkoptsub  22805  grpodivfval  28896  pstmval  31845  sxsigon  32160  cndprobval  32400  dfrngc2  45530  funcrngcsetc  45556  dfringc2  45576  funcringcsetc  45593  lmod1lem1  45828  lmod1lem2  45829  lmod1lem3  45830  lmod1lem4  45831  lmod1lem5  45832  2arymaptfv  45997  2arymaptfo  46000