Theorem trss 5225

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3914  Tr wtr 5214

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-ss 3931  df-uni 4872  df-tr 5215

This theorem is referenced by:  trin  5226  triun  5229  triin  5231  trintss  5233  tz7.2  5621  trpred  6304  ordelss  6348  ordelord  6354  tz7.7  6358  trsucss  6422  tc2  9695  tcel  9698  r1ord3g  9732  r1ord2  9734  r1pwss  9737  rankwflemb  9746  r1elwf  9749  r1elssi  9758  uniwf  9772  itunitc1  10373  wunelss  10661  tskr1om2  10721  tskuni  10736  tskurn  10742  gruelss  10747  dfon2lem6  35776  dfon2lem9  35779  setindtr  43013  dford3lem1  43015  ordelordALT  44527  trsspwALT  44807  trsspwALT2  44808  trsspwALT3  44809  pwtrVD  44813  ordelordALTVD  44856  ralabso  44958  rexabso  44959  modelaxrep  44971  omelaxinf2  44979