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

Theorem trss 5184
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 5179 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 3940 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3546 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 220 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  wral 3062  wss 3880  Tr wtr 5175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-11 2159  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-v 3422  df-in 3887  df-ss 3897  df-uni 4834  df-tr 5176
This theorem is referenced by:  trin  5185  triun  5188  triin  5190  trintss  5192  tz7.2  5549  trpred  6206  ordelss  6246  ordelord  6252  tz7.7  6256  trsucss  6315  omsindsOLD  7684  tc2  9382  tcel  9385  r1ord3g  9419  r1ord2  9421  r1pwss  9424  rankwflemb  9433  r1elwf  9436  r1elssi  9445  uniwf  9459  itunitc1  10058  wunelss  10346  tskr1om2  10406  tskuni  10421  tskurn  10427  gruelss  10432  dfon2lem6  33506  dfon2lem9  33509  setindtr  40577  dford3lem1  40579  ordelordALT  41858  trsspwALT  42139  trsspwALT2  42140  trsspwALT3  42141  pwtrVD  42145  ordelordALTVD  42188
  Copyright terms: Public domain W3C validator