Theorem trss 5221

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

Syntax hints:   → wi 4   ∈ wcel 2145  ∀wral 3079   ⊆ wss 3907  Tr wtr 5211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-v 3459  df-ss 3924  df-uni 4868  df-tr 5212

This theorem is referenced by:  trun  5222  trin  5223  triun  5226  triin  5228  trintss  5230  tz7.2  5634  trpred  6321  ordelss  6365  ordelord  6371  tz7.7  6375  trsucss  6440  tc2  9697  tcel  9700  r1ord3g  9739  r1ord2  9741  r1pwss  9744  rankwflemb  9753  r1elwf  9756  r1elssi  9765  uniwf  9779  itunitc1  10392  wunelss  10681  tskr1om2  10741  tskuni  10756  tskurn  10762  gruelss  10767  tz9.1regs  35437  dfon2lem6  36144  dfon2lem9  36147  axtco2g  36845  tr0elw  36852  tr0el  36853  ttctr2  36862  ttciunun  36879  setindtr  43608  dford3lem1  43610  ordelordALT  45105  trsspwALT  45385  trsspwALT2  45386  trsspwALT3  45387  pwtrVD  45391  ordelordALTVD  45434  ralabso  45536  rexabso  45537  modelaxrep  45549  omelaxinf2  45557