Theorem trss 5294

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 5289	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 4034	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3632	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 217	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3067   ⊆ wss 3976  Tr wtr 5283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284

This theorem is referenced by:  trin  5295  triun  5298  triin  5300  trintss  5302  tz7.2  5683  trpred  6363  ordelss  6411  ordelord  6417  tz7.7  6421  trsucss  6483  omsindsOLD  7925  tc2  9811  tcel  9814  r1ord3g  9848  r1ord2  9850  r1pwss  9853  rankwflemb  9862  r1elwf  9865  r1elssi  9874  uniwf  9888  itunitc1  10489  wunelss  10777  tskr1om2  10837  tskuni  10852  tskurn  10858  gruelss  10863  dfon2lem6  35752  dfon2lem9  35755  setindtr  42981  dford3lem1  42983  ordelordALT  44508  trsspwALT  44789  trsspwALT2  44790  trsspwALT3  44791  pwtrVD  44795  ordelordALTVD  44838