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

Theorem trss 5172
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 5167 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 3989 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3617 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 218 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wral 3135  wss 3933  Tr wtr 5163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-v 3494  df-in 3940  df-ss 3949  df-uni 4831  df-tr 5164
This theorem is referenced by:  trin  5173  triun  5176  triin  5178  trintss  5180  tz7.2  5532  ordelss  6200  ordelord  6206  tz7.7  6210  trsucss  6269  omsinds  7589  tc2  9172  tcel  9175  r1ord3g  9196  r1ord2  9198  r1pwss  9201  rankwflemb  9210  r1elwf  9213  r1elssi  9222  uniwf  9236  itunitc1  9830  wunelss  10118  tskr1om2  10178  tskuni  10193  tskurn  10199  gruelss  10204  dfon2lem6  32930  dfon2lem9  32933  setindtr  39499  dford3lem1  39501  ordelordALT  40748  trsspwALT  41029  trsspwALT2  41030  trsspwALT3  41031  pwtrVD  41035  ordelordALTVD  41078
  Copyright terms: Public domain W3C validator