Theorem trss 5215

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3051   ⊆ wss 3901  Tr wtr 5205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206

This theorem is referenced by:  trin  5216  triun  5219  triin  5221  trintss  5223  tz7.2  5607  trpred  6289  ordelss  6333  ordelord  6339  tz7.7  6343  trsucss  6407  tc2  9649  tcel  9652  r1ord3g  9691  r1ord2  9693  r1pwss  9696  rankwflemb  9705  r1elwf  9708  r1elssi  9717  uniwf  9731  itunitc1  10330  wunelss  10619  tskr1om2  10679  tskuni  10694  tskurn  10700  gruelss  10705  tz9.1regs  35290  dfon2lem6  35980  dfon2lem9  35983  exeltr  36665  setindtr  43266  dford3lem1  43268  ordelordALT  44778  trsspwALT  45058  trsspwALT2  45059  trsspwALT3  45060  pwtrVD  45064  ordelordALTVD  45107  ralabso  45209  rexabso  45210  modelaxrep  45222  omelaxinf2  45230