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 5179 | . 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | |
2 | sseq1 3940 | . . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) | |
3 | 2 | rspccv 3546 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | sylbi 220 | 1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 ∀wral 3062 ⊆ wss 3880 Tr wtr 5175 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-11 2159 ax-ext 2709 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-v 3422 df-in 3887 df-ss 3897 df-uni 4834 df-tr 5176 |
This theorem is referenced by: trin 5185 triun 5188 triin 5190 trintss 5192 tz7.2 5549 trpred 6206 ordelss 6246 ordelord 6252 tz7.7 6256 trsucss 6315 omsindsOLD 7684 tc2 9382 tcel 9385 r1ord3g 9419 r1ord2 9421 r1pwss 9424 rankwflemb 9433 r1elwf 9436 r1elssi 9445 uniwf 9459 itunitc1 10058 wunelss 10346 tskr1om2 10406 tskuni 10421 tskurn 10427 gruelss 10432 dfon2lem6 33506 dfon2lem9 33509 setindtr 40577 dford3lem1 40579 ordelordALT 41858 trsspwALT 42139 trsspwALT2 42140 trsspwALT3 42141 pwtrVD 42145 ordelordALTVD 42188 |
Copyright terms: Public domain | W3C validator |