Theorem trss 5145

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 5140	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3940	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3568	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 220	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106   ⊆ wss 3881  Tr wtr 5136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-tr 5137

This theorem is referenced by:  trin  5146  triun  5149  triin  5151  trintss  5153  tz7.2  5503  ordelss  6175  ordelord  6181  tz7.7  6185  trsucss  6244  omsinds  7580  tc2  9168  tcel  9171  r1ord3g  9192  r1ord2  9194  r1pwss  9197  rankwflemb  9206  r1elwf  9209  r1elssi  9218  uniwf  9232  itunitc1  9831  wunelss  10119  tskr1om2  10179  tskuni  10194  tskurn  10200  gruelss  10205  dfon2lem6  33146  dfon2lem9  33149  setindtr  39965  dford3lem1  39967  ordelordALT  41243  trsspwALT  41524  trsspwALT2  41525  trsspwALT3  41526  pwtrVD  41530  ordelordALTVD  41573