Theorem trss 5212

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 5207	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3956	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3570	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 217	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3048   ⊆ wss 3898  Tr wtr 5202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-v 3439  df-ss 3915  df-uni 4861  df-tr 5203

This theorem is referenced by:  trin  5213  triun  5216  triin  5218  trintss  5220  tz7.2  5604  trpred  6285  ordelss  6329  ordelord  6335  tz7.7  6339  trsucss  6403  tc2  9639  tcel  9642  r1ord3g  9681  r1ord2  9683  r1pwss  9686  rankwflemb  9695  r1elwf  9698  r1elssi  9707  uniwf  9721  itunitc1  10320  wunelss  10608  tskr1om2  10668  tskuni  10683  tskurn  10689  gruelss  10694  tz9.1regs  35153  dfon2lem6  35853  dfon2lem9  35856  setindtr  43144  dford3lem1  43146  ordelordALT  44657  trsspwALT  44937  trsspwALT2  44938  trsspwALT3  44939  pwtrVD  44943  ordelordALTVD  44986  ralabso  45088  rexabso  45089  modelaxrep  45101  omelaxinf2  45109