Theorem trss 5240

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3051   ⊆ wss 3926  Tr wtr 5229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230

This theorem is referenced by:  trin  5241  triun  5244  triin  5246  trintss  5248  tz7.2  5637  trpred  6320  ordelss  6368  ordelord  6374  tz7.7  6378  trsucss  6442  tc2  9756  tcel  9759  r1ord3g  9793  r1ord2  9795  r1pwss  9798  rankwflemb  9807  r1elwf  9810  r1elssi  9819  uniwf  9833  itunitc1  10434  wunelss  10722  tskr1om2  10782  tskuni  10797  tskurn  10803  gruelss  10808  dfon2lem6  35806  dfon2lem9  35809  setindtr  43048  dford3lem1  43050  ordelordALT  44562  trsspwALT  44842  trsspwALT2  44843  trsspwALT3  44844  pwtrVD  44848  ordelordALTVD  44891  ralabso  44993  rexabso  44994  modelaxrep  45006  omelaxinf2  45014