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

Theorem trss 4721
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 4716 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 3605 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3292 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 207 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wral 2907  wss 3555  Tr wtr 4712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-v 3188  df-in 3562  df-ss 3569  df-uni 4403  df-tr 4713
This theorem is referenced by:  trin  4723  triun  4726  trintss  4729  tz7.2  5058  ordelss  5698  ordelord  5704  tz7.7  5708  trsucss  5770  omsinds  7031  tc2  8562  tcel  8565  r1ord3g  8586  r1ord2  8588  r1pwss  8591  rankwflemb  8600  r1elwf  8603  r1elssi  8612  uniwf  8626  itunitc1  9186  wunelss  9474  tskr1om2  9534  tskuni  9549  tskurn  9555  gruelss  9560  dfon2lem6  31391  dfon2lem9  31394  setindtr  37068  dford3lem1  37070  ordelordALT  38226  trsspwALT  38525  trsspwALT2  38526  trsspwALT3  38527  pwtrVD  38539  ordelordALTVD  38583
  Copyright terms: Public domain W3C validator