Theorem trss 5229

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 5224	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3963	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3579	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 220	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2143  ∀wral 3079   ⊆ wss 3906  Tr wtr 5219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-ss 3923  df-uni 4874  df-tr 5220

This theorem is referenced by:  trun  5230  trin  5231  triun  5234  triin  5236  trintss  5238  tz7.2  5646  trpred  6334  ordelss  6378  ordelord  6384  tz7.7  6388  trsucss  6453  tc2  9710  tcel  9713  r1ord3g  9752  r1ord2  9754  r1pwss  9757  rankwflemb  9766  r1elwf  9769  r1elssi  9778  uniwf  9792  itunitc1  10405  wunelss  10694  tskr1om2  10754  tskuni  10769  tskurn  10775  gruelss  10780  tz9.1regs  35528  dfon2lem6  36259  dfon2lem9  36262  nmuladdss  36671  axtco2g  36969  tr0elw  36976  tr0el  36977  ttctr2  36986  ttciunun  37003  setindtr  43734  dford3lem1  43736  ordelordALT  45229  trsspwALT  45509  trsspwALT2  45510  trsspwALT3  45511  pwtrVD  45515  ordelordALTVD  45558  ralabso  45660  rexabso  45661  modelaxrep  45673  omelaxinf2  45681