Theorem trss 5275

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∀wral 3058   ⊆ wss 3962  Tr wtr 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-v 3479  df-ss 3979  df-uni 4912  df-tr 5265

This theorem is referenced by:  trin  5276  triun  5279  triin  5281  trintss  5283  tz7.2  5671  trpred  6353  ordelss  6401  ordelord  6407  tz7.7  6411  trsucss  6473  omsindsOLD  7908  tc2  9779  tcel  9782  r1ord3g  9816  r1ord2  9818  r1pwss  9821  rankwflemb  9830  r1elwf  9833  r1elssi  9842  uniwf  9856  itunitc1  10457  wunelss  10745  tskr1om2  10805  tskuni  10820  tskurn  10826  gruelss  10831  dfon2lem6  35769  dfon2lem9  35772  setindtr  43012  dford3lem1  43014  ordelordALT  44534  trsspwALT  44815  trsspwALT2  44816  trsspwALT3  44817  pwtrVD  44821  ordelordALTVD  44864  modelaxrep  44945