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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3905  Tr wtr 5202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-ss 3922  df-uni 4862  df-tr 5203

This theorem is referenced by:  trin  5213  triun  5216  triin  5218  trintss  5220  tz7.2  5606  trpred  6283  ordelss  6327  ordelord  6333  tz7.7  6337  trsucss  6401  tc2  9657  tcel  9660  r1ord3g  9694  r1ord2  9696  r1pwss  9699  rankwflemb  9708  r1elwf  9711  r1elssi  9720  uniwf  9734  itunitc1  10333  wunelss  10621  tskr1om2  10681  tskuni  10696  tskurn  10702  gruelss  10707  tz9.1regs  35069  dfon2lem6  35764  dfon2lem9  35767  setindtr  43000  dford3lem1  43002  ordelordALT  44514  trsspwALT  44794  trsspwALT2  44795  trsspwALT3  44796  pwtrVD  44800  ordelordALTVD  44843  ralabso  44945  rexabso  44946  modelaxrep  44958  omelaxinf2  44966