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

Theorem trss 4895
Description: An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) (Proof shortened by JJ, 26-Jul-2021.)
Assertion
Ref Expression
trss (Tr 𝐴 → (𝐵𝐴𝐵𝐴))

Proof of Theorem trss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dftr3 4890 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 3775 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3457 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 207 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wral 3061  wss 3723  Tr wtr 4886
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-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353  df-in 3730  df-ss 3737  df-uni 4575  df-tr 4887
This theorem is referenced by:  trin  4896  triun  4899  trintss  4902  tz7.2  5233  ordelss  5882  ordelord  5888  tz7.7  5892  trsucss  5954  omsinds  7231  tc2  8782  tcel  8785  r1ord3g  8806  r1ord2  8808  r1pwss  8811  rankwflemb  8820  r1elwf  8823  r1elssi  8832  uniwf  8846  itunitc1  9444  wunelss  9732  tskr1om2  9792  tskuni  9807  tskurn  9813  gruelss  9818  dfon2lem6  32029  dfon2lem9  32032  setindtr  38117  dford3lem1  38119  ordelordALT  39272  trsspwALT  39570  trsspwALT2  39571  trsspwALT3  39572  pwtrVD  39581  ordelordALTVD  39625
  Copyright terms: Public domain W3C validator