MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coexg Structured version   Visualization version   GIF version

Theorem coexg 7867
Description: The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
Assertion
Ref Expression
coexg ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)

Proof of Theorem coexg
StepHypRef Expression
1 cossxp 6225 . 2 (𝐴𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2 dmexg 7841 . . 3 (𝐵𝑊 → dom 𝐵 ∈ V)
3 rnexg 7842 . . 3 (𝐴𝑉 → ran 𝐴 ∈ V)
4 xpexg 7685 . . 3 ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
52, 3, 4syl2anr 598 . 2 ((𝐴𝑉𝐵𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6 ssexg 5281 . 2 (((𝐴𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴𝐵) ∈ V)
71, 5, 6sylancr 588 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  Vcvv 3444  wss 3911   × cxp 5632  dom cdm 5634  ran crn 5635  ccom 5638
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645
This theorem is referenced by:  coex  7868  suppco  8138  fsuppco2  9344  fsuppcor  9345  mapfienlem2  9347  wemapwe  9638  cofsmo  10210  relexpsucnnr  14916  supcvg  15746  imasle  17410  setcco  17974  estrcco  18022  pwsco1mhm  18647  pwsco2mhm  18648  efmndov  18696  efmndcl  18697  symgov  19170  symgcl  19171  gsumval3lem2  19688  gsumzf1o  19694  f1lindf  21244  evls1sca  21705  tngds  24027  tngdsOLD  24028  climcncf  24279  motplusg  27526  tocycfv  32007  smatfval  32433  eulerpartlemmf  33032  hgt750lemg  33324  cossex  36927  tgrpov  39257  erngmul  39315  erngmul-rN  39323  dvamulr  39521  dvavadd  39524  dvhmulr  39595  coexd  40699  mendmulr  41558  relexp0a  42076  choicefi  43508  climexp  43932  dvsinax  44240  stoweidlem27  44354  stoweidlem31  44358  stoweidlem59  44386  uspgrbisymrelALT  46143  rngccoALTV  46372  ringccoALTV  46435  itcoval1  46835  itcoval2  46836  itcoval3  46837  itcovalsucov  46840
  Copyright terms: Public domain W3C validator