Theorem trss 5228

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3045   ⊆ wss 3917  Tr wtr 5217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218

This theorem is referenced by:  trin  5229  triun  5232  triin  5234  trintss  5236  tz7.2  5624  trpred  6307  ordelss  6351  ordelord  6357  tz7.7  6361  trsucss  6425  tc2  9702  tcel  9705  r1ord3g  9739  r1ord2  9741  r1pwss  9744  rankwflemb  9753  r1elwf  9756  r1elssi  9765  uniwf  9779  itunitc1  10380  wunelss  10668  tskr1om2  10728  tskuni  10743  tskurn  10749  gruelss  10754  dfon2lem6  35783  dfon2lem9  35786  setindtr  43020  dford3lem1  43022  ordelordALT  44534  trsspwALT  44814  trsspwALT2  44815  trsspwALT3  44816  pwtrVD  44820  ordelordALTVD  44863  ralabso  44965  rexabso  44966  modelaxrep  44978  omelaxinf2  44986