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

Theorem coexg 7264
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 5802 . 2 (𝐴𝐵) ⊆ (dom 𝐵 × ran 𝐴)
2 dmexg 7244 . . 3 (𝐵𝑊 → dom 𝐵 ∈ V)
3 rnexg 7245 . . 3 (𝐴𝑉 → ran 𝐴 ∈ V)
4 xpexg 7107 . . 3 ((dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V) → (dom 𝐵 × ran 𝐴) ∈ V)
52, 3, 4syl2anr 576 . 2 ((𝐴𝑉𝐵𝑊) → (dom 𝐵 × ran 𝐴) ∈ V)
6 ssexg 4938 . 2 (((𝐴𝐵) ⊆ (dom 𝐵 × ran 𝐴) ∧ (dom 𝐵 × ran 𝐴) ∈ V) → (𝐴𝐵) ∈ V)
71, 5, 6sylancr 567 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  Vcvv 3351  wss 3723   × cxp 5247  dom cdm 5249  ran crn 5250  ccom 5253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260
This theorem is referenced by:  coex  7265  supp0cosupp0  7486  imacosupp  7487  fsuppco2  8464  fsuppcor  8465  mapfienlem2  8467  wemapwe  8758  cofsmo  9293  relexpsucnnr  13973  supcvg  14795  imasle  16391  setcco  16940  estrcco  16977  pwsco1mhm  17578  pwsco2mhm  17579  symgov  18017  symgcl  18018  gsumval3lem2  18514  gsumzf1o  18520  evls1sca  19903  f1lindf  20378  tngds  22672  climcncf  22923  motplusg  25658  smatfval  30201  eulerpartlemmf  30777  hgt750lemg  31072  cossex  34516  tgrpov  36557  erngmul  36615  erngmul-rN  36623  dvamulr  36821  dvavadd  36824  dvhmulr  36896  mendmulr  38284  relexp0a  38534  choicefi  39910  climexp  40355  dvsinax  40645  stoweidlem27  40761  stoweidlem31  40765  stoweidlem59  40793  uspgrbisymrelALT  42291  rngccoALTV  42516  ringccoALTV  42579
  Copyright terms: Public domain W3C validator