Theorem trss 5230

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∀wral 3081   ⊆ wss 3906  Tr wtr 5220

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 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221

This theorem is used by:  trun  5231  trin  5232  triun  5235  triin  5237  trintss  5239  tz7.2  5646  trpred  6336  ordelss  6380  ordelord  6386  tz7.7  6390  trsucss  6455  tc2  9712  tcel  9715  r1ord3g  9754  r1ord2  9756  r1pwss  9759  rankwflemb  9768  r1elwf  9771  r1elssi  9780  uniwf  9794  itunitc1  10415  wunelss  10704  tskr1om2  10764  tskuni  10779  tskurn  10785  gruelss  10790  tz9.1regs  35563  dfon2lem6  36291  dfon2lem9  36294  nmuladdss  36718  axtco2g  37021  tr0elw  37028  tr0el  37029  ttctr2  37038  ttciunun  37055  setindtr  43784  dford3lem1  43786  ordelordALT  45279  trsspwALT  45559  trsspwALT2  45560  trsspwALT3  45561  pwtrVD  45565  ordelordALTVD  45608  ralabso  45710  rexabso  45711  modelaxrep  45723  omelaxinf2  45731