Theorem trss 5208

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3047   ⊆ wss 3902  Tr wtr 5198

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-ss 3919  df-uni 4860  df-tr 5199

This theorem is referenced by:  trin  5209  triun  5212  triin  5214  trintss  5216  tz7.2  5599  trpred  6278  ordelss  6322  ordelord  6328  tz7.7  6332  trsucss  6396  tc2  9630  tcel  9633  r1ord3g  9672  r1ord2  9674  r1pwss  9677  rankwflemb  9686  r1elwf  9689  r1elssi  9698  uniwf  9712  itunitc1  10311  wunelss  10599  tskr1om2  10659  tskuni  10674  tskurn  10680  gruelss  10685  tz9.1regs  35128  dfon2lem6  35828  dfon2lem9  35831  setindtr  43063  dford3lem1  43065  ordelordALT  44576  trsspwALT  44856  trsspwALT2  44857  trsspwALT3  44858  pwtrVD  44862  ordelordALTVD  44905  ralabso  45007  rexabso  45008  modelaxrep  45020  omelaxinf2  45028