![]() |
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 5275 | . 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | |
2 | sseq1 4004 | . . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) | |
3 | 2 | rspccv 3604 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | sylbi 216 | 1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |