Theorem trss 5196

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 5191	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3947	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3564	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 218	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2119  ∀wral 3054   ⊆ wss 3890  Tr wtr 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-v 3434  df-ss 3907  df-uni 4846  df-tr 5187

This theorem is referenced by:  trun  5197  trin  5198  triun  5201  triin  5203  trintss  5205  tz7.2  5608  trpred  6289  ordelss  6333  ordelord  6339  tz7.7  6343  trsucss  6407  tc2  9659  tcel  9662  r1ord3g  9701  r1ord2  9703  r1pwss  9706  rankwflemb  9715  r1elwf  9718  r1elssi  9727  uniwf  9741  itunitc1  10340  wunelss  10629  tskr1om2  10689  tskuni  10704  tskurn  10710  gruelss  10715  tz9.1regs  35322  dfon2lem6  36021  dfon2lem9  36024  axtco2g  36712  tr0elw  36719  tr0el  36720  ttctr2  36729  ttciunun  36746  setindtr  43476  dford3lem1  43478  ordelordALT  44988  trsspwALT  45268  trsspwALT2  45269  trsspwALT3  45270  pwtrVD  45274  ordelordALTVD  45317  ralabso  45419  rexabso  45420  modelaxrep  45432  omelaxinf2  45440