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

Theorem trss 5230
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 5225 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
2 sseq1 3963 . . 3 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
32rspccv 3580 . 2 (∀𝑥𝐴 𝑥𝐴 → (𝐵𝐴𝐵𝐴))
41, 3sylbi 220 1 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wcel 2146  wral 3081  wss 3906  Tr wtr 5220
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737
This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221
This theorem is used by:  trun  5231  trin  5232  triun  5235  triin  5237  trintss  5239  tz7.2  5646  trpred  6336  ordelss  6380  ordelord  6386  tz7.7  6390  trsucss  6455  tc2  9712  tcel  9715  r1ord3g  9754  r1ord2  9756  r1pwss  9759  rankwflemb  9768  r1elwf  9771  r1elssi  9780  uniwf  9794  itunitc1  10415  wunelss  10704  tskr1om2  10764  tskuni  10779  tskurn  10785  gruelss  10790  tz9.1regs  35563  dfon2lem6  36291  dfon2lem9  36294  nmuladdss  36718  axtco2g  37021  tr0elw  37028  tr0el  37029  ttctr2  37038  ttciunun  37055  setindtr  43784  dford3lem1  43786  ordelordALT  45279  trsspwALT  45559  trsspwALT2  45560  trsspwALT3  45561  pwtrVD  45565  ordelordALTVD  45608  ralabso  45710  rexabso  45711  modelaxrep  45723  omelaxinf2  45731
  Copyright terms: Public domain W3C validator