![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > trss | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
trss | ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dftr3 5232 | . 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | |
2 | sseq1 3973 | . . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) | |
3 | 2 | rspccv 3580 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | sylbi 216 | 1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ∀wral 3061 ⊆ wss 3914 Tr wtr 5226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-v 3449 df-in 3921 df-ss 3931 df-uni 4870 df-tr 5227 |
This theorem is referenced by: trin 5238 triun 5241 triin 5243 trintss 5245 tz7.2 5621 trpred 6289 ordelss 6337 ordelord 6343 tz7.7 6347 trsucss 6409 omsindsOLD 7828 tc2 9686 tcel 9689 r1ord3g 9723 r1ord2 9725 r1pwss 9728 rankwflemb 9737 r1elwf 9740 r1elssi 9749 uniwf 9763 itunitc1 10364 wunelss 10652 tskr1om2 10712 tskuni 10727 tskurn 10733 gruelss 10738 dfon2lem6 34426 dfon2lem9 34429 setindtr 41395 dford3lem1 41397 ordelordALT 42911 trsspwALT 43192 trsspwALT2 43193 trsspwALT3 43194 pwtrVD 43198 ordelordALTVD 43241 |
Copyright terms: Public domain | W3C validator |