Theorem trss 5228

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080   ⊆ wss 3900  Tr wtr 5218

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-ss 3901  df-uni 4873  df-tr 5219

This theorem is used by:  trun  5229  trin  5230  triun  5233  triin  5235  trintss  5237  tz7.2  5641  trpred  6360  ordelss  6404  ordelord  6410  tz7.7  6414  trsucss  6479  tc2  9778  tcel  9781  r1ord3g  9823  r1ord2  9825  r1pwss  9828  rankwflemb  9837  rankwflembOLD  9838  r1elwf  9841  r1elssi  9850  uniwf  9865  itunitc1  10537  wunelss  10832  tskhf  10892  tskuni  10907  tskurn  10913  gruelss  10918  tz9.1regs  35943  dfon2lem6  36765  dfon2lem9  36768  nmuladdss  37177  axtco2g  37480  tr0elw  37487  tr0el  37488  ttctr2  37497  ttciunun  37514  setindtr  44297  dford3lem1  44299  ordelordALT  45780  trsspwALT  46060  trsspwALT2  46061  trsspwALT3  46062  pwtrVD  46066  ordelordALTVD  46109  ralabso  46222  rexabso  46223  modelaxrep  46235  omelaxinf2  46243