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

Theorem trss 5280
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 5275 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 4004 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3604 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 216 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2098  wral 3050  wss 3946  Tr wtr 5269
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3963  df-uni 4913  df-tr 5270
This theorem is referenced by:  trin  5281  triun  5284  triin  5286  trintss  5288  tz7.2  5665  trpred  6343  ordelss  6391  ordelord  6397  tz7.7  6401  trsucss  6463  omsindsOLD  7897  tc2  9781  tcel  9784  r1ord3g  9818  r1ord2  9820  r1pwss  9823  rankwflemb  9832  r1elwf  9835  r1elssi  9844  uniwf  9858  itunitc1  10459  wunelss  10747  tskr1om2  10807  tskuni  10822  tskurn  10828  gruelss  10833  dfon2lem6  35572  dfon2lem9  35575  setindtr  42631  dford3lem1  42633  ordelordALT  44162  trsspwALT  44443  trsspwALT2  44444  trsspwALT3  44445  pwtrVD  44449  ordelordALTVD  44492
  Copyright terms: Public domain W3C validator