Theorem trss 4689

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 4684	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 3589	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3279	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 206	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540  Tr wtr 4680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373  df-tr 4681

This theorem is referenced by:  trin  4691  triun  4694  trint0  4698  tz7.2  5022  ordelss  5656  ordelord  5662  tz7.7  5666  trsucss  5728  omsinds  6976  tc2  8501  tcel  8504  r1ord3g  8525  r1ord2  8527  r1pwss  8530  rankwflemb  8539  r1elwf  8542  r1elssi  8551  uniwf  8565  itunitc1  9125  wunelss  9409  tskr1om2  9469  tskuni  9484  tskurn  9490  gruelss  9495  dfon2lem6  30937  dfon2lem9  30940  setindtr  36609  dford3lem1  36611  ordelordALT  37768  trsspwALT  38067  trsspwALT2  38068  trsspwALT3  38069  pwtrVD  38081  ordelordALTVD  38125