Theorem trss 5200

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 5195	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3946	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3558	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 216	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064   ⊆ wss 3887  Tr wtr 5191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-tr 5192

This theorem is referenced by:  trin  5201  triun  5204  triin  5206  trintss  5208  tz7.2  5573  trpred  6234  ordelss  6282  ordelord  6288  tz7.7  6292  trsucss  6351  omsindsOLD  7734  tc2  9500  tcel  9503  r1ord3g  9537  r1ord2  9539  r1pwss  9542  rankwflemb  9551  r1elwf  9554  r1elssi  9563  uniwf  9577  itunitc1  10176  wunelss  10464  tskr1om2  10524  tskuni  10539  tskurn  10545  gruelss  10550  dfon2lem6  33764  dfon2lem9  33767  setindtr  40846  dford3lem1  40848  ordelordALT  42157  trsspwALT  42438  trsspwALT2  42439  trsspwALT3  42440  pwtrVD  42444  ordelordALTVD  42487