Theorem trss 5196

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063   ⊆ wss 3883  Tr wtr 5187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-tr 5188

This theorem is referenced by:  trin  5197  triun  5200  triin  5202  trintss  5204  tz7.2  5564  trpred  6223  ordelss  6267  ordelord  6273  tz7.7  6277  trsucss  6336  omsindsOLD  7709  tc2  9431  tcel  9434  r1ord3g  9468  r1ord2  9470  r1pwss  9473  rankwflemb  9482  r1elwf  9485  r1elssi  9494  uniwf  9508  itunitc1  10107  wunelss  10395  tskr1om2  10455  tskuni  10470  tskurn  10476  gruelss  10481  dfon2lem6  33670  dfon2lem9  33673  setindtr  40762  dford3lem1  40764  ordelordALT  42046  trsspwALT  42327  trsspwALT2  42328  trsspwALT3  42329  pwtrVD  42333  ordelordALTVD  42376