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

Theorem trss 5237
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 5232 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 3973 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3580 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 216 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3061  wss 3914  Tr wtr 5226
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-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-v 3449  df-in 3921  df-ss 3931  df-uni 4870  df-tr 5227
This theorem is referenced by:  trin  5238  triun  5241  triin  5243  trintss  5245  tz7.2  5621  trpred  6289  ordelss  6337  ordelord  6343  tz7.7  6347  trsucss  6409  omsindsOLD  7828  tc2  9686  tcel  9689  r1ord3g  9723  r1ord2  9725  r1pwss  9728  rankwflemb  9737  r1elwf  9740  r1elssi  9749  uniwf  9763  itunitc1  10364  wunelss  10652  tskr1om2  10712  tskuni  10727  tskurn  10733  gruelss  10738  dfon2lem6  34426  dfon2lem9  34429  setindtr  41395  dford3lem1  41397  ordelordALT  42911  trsspwALT  43192  trsspwALT2  43193  trsspwALT3  43194  pwtrVD  43198  ordelordALTVD  43241
  Copyright terms: Public domain W3C validator