Theorem trss 5217

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3903  Tr wtr 5207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-ss 3920  df-uni 4866  df-tr 5208

This theorem is referenced by:  trin  5218  triun  5221  triin  5223  trintss  5225  tz7.2  5615  trpred  6297  ordelss  6341  ordelord  6347  tz7.7  6351  trsucss  6415  tc2  9661  tcel  9664  r1ord3g  9703  r1ord2  9705  r1pwss  9708  rankwflemb  9717  r1elwf  9720  r1elssi  9729  uniwf  9743  itunitc1  10342  wunelss  10631  tskr1om2  10691  tskuni  10706  tskurn  10712  gruelss  10717  tz9.1regs  35309  dfon2lem6  35999  dfon2lem9  36002  exeltr  36684  setindtr  43378  dford3lem1  43380  ordelordALT  44890  trsspwALT  45170  trsspwALT2  45171  trsspwALT3  45172  pwtrVD  45176  ordelordALTVD  45219  ralabso  45321  rexabso  45322  modelaxrep  45334  omelaxinf2  45342