Theorem trss 5203

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

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

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 3432  df-ss 3907  df-uni 4852  df-tr 5194

This theorem is referenced by:  trin  5204  triun  5207  triin  5209  trintss  5211  tz7.2  5607  trpred  6289  ordelss  6333  ordelord  6339  tz7.7  6343  trsucss  6407  tc2  9652  tcel  9655  r1ord3g  9694  r1ord2  9696  r1pwss  9699  rankwflemb  9708  r1elwf  9711  r1elssi  9720  uniwf  9734  itunitc1  10333  wunelss  10622  tskr1om2  10682  tskuni  10697  tskurn  10703  gruelss  10708  tz9.1regs  35294  dfon2lem6  35984  dfon2lem9  35987  axtco2g  36675  tr0elw  36682  tr0el  36683  ttctr2  36692  ttciunun  36709  setindtr  43470  dford3lem1  43472  ordelordALT  44982  trsspwALT  45262  trsspwALT2  45263  trsspwALT3  45264  pwtrVD  45268  ordelordALTVD  45311  ralabso  45413  rexabso  45414  modelaxrep  45426  omelaxinf2  45434