Theorem trss 4895

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 4890	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3775	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3457	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 207	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2145  ∀wral 3061   ⊆ wss 3723  Tr wtr 4886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353  df-in 3730  df-ss 3737  df-uni 4575  df-tr 4887

This theorem is referenced by:  trin  4896  triun  4899  trintss  4902  tz7.2  5233  ordelss  5882  ordelord  5888  tz7.7  5892  trsucss  5954  omsinds  7231  tc2  8782  tcel  8785  r1ord3g  8806  r1ord2  8808  r1pwss  8811  rankwflemb  8820  r1elwf  8823  r1elssi  8832  uniwf  8846  itunitc1  9444  wunelss  9732  tskr1om2  9792  tskuni  9807  tskurn  9813  gruelss  9818  dfon2lem6  32029  dfon2lem9  32032  setindtr  38117  dford3lem1  38119  ordelordALT  39272  trsspwALT  39570  trsspwALT2  39571  trsspwALT3  39572  pwtrVD  39581  ordelordALTVD  39625