Theorem trss 5214

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 3075   ⊆ wss 3902  Tr wtr 5204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-v 3455  df-ss 3919  df-uni 4863  df-tr 5205

This theorem is referenced by:  trun  5215  trin  5216  triun  5219  triin  5221  trintss  5223  tz7.2  5626  trpred  6312  ordelss  6356  ordelord  6362  tz7.7  6366  trsucss  6430  tc2  9688  tcel  9691  r1ord3g  9730  r1ord2  9732  r1pwss  9735  rankwflemb  9744  r1elwf  9747  r1elssi  9756  uniwf  9770  itunitc1  10370  wunelss  10659  tskr1om2  10719  tskuni  10734  tskurn  10740  gruelss  10745  tz9.1regs  35390  dfon2lem6  36096  dfon2lem9  36099  axtco2g  36797  tr0elw  36804  tr0el  36805  ttctr2  36814  ttciunun  36831  setindtr  43561  dford3lem1  43563  ordelordALT  45073  trsspwALT  45353  trsspwALT2  45354  trsspwALT3  45355  pwtrVD  45359  ordelordALTVD  45402  ralabso  45504  rexabso  45505  modelaxrep  45517  omelaxinf2  45525