Theorem trss 5276

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3061   ⊆ wss 3948  Tr wtr 5265

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266

This theorem is referenced by:  trin  5277  triun  5280  triin  5282  trintss  5284  tz7.2  5660  trpred  6332  ordelss  6380  ordelord  6386  tz7.7  6390  trsucss  6452  omsindsOLD  7876  tc2  9736  tcel  9739  r1ord3g  9773  r1ord2  9775  r1pwss  9778  rankwflemb  9787  r1elwf  9790  r1elssi  9799  uniwf  9813  itunitc1  10414  wunelss  10702  tskr1om2  10762  tskuni  10777  tskurn  10783  gruelss  10788  dfon2lem6  34755  dfon2lem9  34758  setindtr  41753  dford3lem1  41755  ordelordALT  43288  trsspwALT  43569  trsspwALT2  43570  trsspwALT3  43571  pwtrVD  43575  ordelordALTVD  43618