Theorem trss 5207

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.

Step	Hyp	Ref	Expression
1		dftr3 5202	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3952	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3569	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 219	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2132  ∀wral 3066   ⊆ wss 3895  Tr wtr 5197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-v 3446  df-ss 3912  df-uni 4856  df-tr 5198

This theorem is referenced by:  trun  5208  trin  5209  triun  5212  triin  5214  trintss  5216  tz7.2  5619  trpred  6303  ordelss  6347  ordelord  6353  tz7.7  6357  trsucss  6421  tc2  9681  tcel  9684  r1ord3g  9723  r1ord2  9725  r1pwss  9728  rankwflemb  9737  r1elwf  9740  r1elssi  9749  uniwf  9763  itunitc1  10363  wunelss  10652  tskr1om2  10712  tskuni  10727  tskurn  10733  gruelss  10738  tz9.1regs  35375  dfon2lem6  36074  dfon2lem9  36077  axtco2g  36775  tr0elw  36782  tr0el  36783  ttctr2  36792  ttciunun  36809  setindtr  43539  dford3lem1  43541  ordelordALT  45051  trsspwALT  45331  trsspwALT2  45332  trsspwALT3  45333  pwtrVD  45337  ordelordALTVD  45380  ralabso  45482  rexabso  45483  modelaxrep  45495  omelaxinf2  45503