Theorem trss 5277

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062   ⊆ wss 3949  Tr wtr 5266

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267

This theorem is referenced by:  trin  5278  triun  5281  triin  5283  trintss  5285  tz7.2  5661  trpred  6333  ordelss  6381  ordelord  6387  tz7.7  6391  trsucss  6453  omsindsOLD  7877  tc2  9737  tcel  9740  r1ord3g  9774  r1ord2  9776  r1pwss  9779  rankwflemb  9788  r1elwf  9791  r1elssi  9800  uniwf  9814  itunitc1  10415  wunelss  10703  tskr1om2  10763  tskuni  10778  tskurn  10784  gruelss  10789  dfon2lem6  34760  dfon2lem9  34763  setindtr  41763  dford3lem1  41765  ordelordALT  43298  trsspwALT  43579  trsspwALT2  43580  trsspwALT3  43581  pwtrVD  43585  ordelordALTVD  43628