Theorem trss 5280

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 5275	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
2		sseq1 4004	. . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴))
3	2	rspccv 3604	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
4	1, 3	sylbi 216	1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2098  ∀wral 3050   ⊆ wss 3946  Tr wtr 5269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3963  df-uni 4913  df-tr 5270

This theorem is referenced by:  trin  5281  triun  5284  triin  5286  trintss  5288  tz7.2  5665  trpred  6343  ordelss  6391  ordelord  6397  tz7.7  6401  trsucss  6463  omsindsOLD  7897  tc2  9781  tcel  9784  r1ord3g  9818  r1ord2  9820  r1pwss  9823  rankwflemb  9832  r1elwf  9835  r1elssi  9844  uniwf  9858  itunitc1  10459  wunelss  10747  tskr1om2  10807  tskuni  10822  tskurn  10828  gruelss  10833  dfon2lem6  35572  dfon2lem9  35575  setindtr  42631  dford3lem1  42633  ordelordALT  44162  trsspwALT  44443  trsspwALT2  44444  trsspwALT3  44445  pwtrVD  44449  ordelordALTVD  44492