Theorem trss 5202

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3051   ⊆ wss 3889  Tr wtr 5192

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-ss 3906  df-uni 4851  df-tr 5193

This theorem is referenced by:  trun  5203  trin  5204  triun  5207  triin  5209  trintss  5211  tz7.2  5614  trpred  6295  ordelss  6339  ordelord  6345  tz7.7  6349  trsucss  6413  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  35278  dfon2lem6  35968  dfon2lem9  35971  axtco2g  36659  tr0elw  36666  tr0el  36667  ttctr2  36676  ttciunun  36693  setindtr  43452  dford3lem1  43454  ordelordALT  44964  trsspwALT  45244  trsspwALT2  45245  trsspwALT3  45246  pwtrVD  45250  ordelordALTVD  45293  ralabso  45395  rexabso  45396  modelaxrep  45408  omelaxinf2  45416