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

Theorem trss 5178
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 5173 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 3996 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3624 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 218 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3143  wss 3940  Tr wtr 5169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-v 3502  df-in 3947  df-ss 3956  df-uni 4838  df-tr 5170
This theorem is referenced by:  trin  5179  triun  5182  triin  5184  trintss  5186  tz7.2  5538  ordelss  6205  ordelord  6211  tz7.7  6215  trsucss  6274  omsinds  7588  tc2  9173  tcel  9176  r1ord3g  9197  r1ord2  9199  r1pwss  9202  rankwflemb  9211  r1elwf  9214  r1elssi  9223  uniwf  9237  itunitc1  9831  wunelss  10119  tskr1om2  10179  tskuni  10194  tskurn  10200  gruelss  10205  dfon2lem6  32920  dfon2lem9  32923  setindtr  39489  dford3lem1  39491  ordelordALT  40739  trsspwALT  41020  trsspwALT2  41021  trsspwALT3  41022  pwtrVD  41026  ordelordALTVD  41069
  Copyright terms: Public domain W3C validator