Theorem trss 5233

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 5228	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3965	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3581	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 220	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∀wral 3082   ⊆ wss 3908  Tr wtr 5223

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-v 3460  df-ss 3925  df-uni 4878  df-tr 5224

This theorem is used by:  trun  5234  trin  5235  triun  5238  triin  5240  trintss  5242  tz7.2  5649  trpred  6339  ordelss  6383  ordelord  6389  tz7.7  6393  trsucss  6458  tc2  9719  tcel  9722  r1ord3g  9761  r1ord2  9763  r1pwss  9766  rankwflemb  9775  r1elwf  9778  r1elssi  9787  uniwf  9801  itunitc1  10422  wunelss  10711  tskr1om2  10771  tskuni  10786  tskurn  10792  gruelss  10797  tz9.1regs  35571  dfon2lem6  36299  dfon2lem9  36302  nmuladdss  36726  axtco2g  37029  tr0elw  37036  tr0el  37037  ttctr2  37046  ttciunun  37063  setindtr  43792  dford3lem1  43794  ordelordALT  45287  trsspwALT  45567  trsspwALT2  45568  trsspwALT3  45569  pwtrVD  45573  ordelordALTVD  45616  ralabso  45718  rexabso  45719  modelaxrep  45731  omelaxinf2  45739