| 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 5228 | . 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | |
| 2 | sseq1 3965 | . . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) | |
| 3 | 2 | rspccv 3581 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
| 4 | 1, 3 | sylbi 220 | 1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∈ wcel 2146 ∀wral 3082 ⊆ wss 3908 Tr wtr 5223 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2738 |
| This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2745 df-cleq 2758 df-clel 2841 df-ral 3083 df-v 3460 df-ss 3925 df-uni 4878 df-tr 5224 |
| This theorem is used by: trun 5234 trin 5235 triun 5238 triin 5240 trintss 5242 tz7.2 5649 trpred 6339 ordelss 6383 ordelord 6389 tz7.7 6393 trsucss 6458 tc2 9719 tcel 9722 r1ord3g 9761 r1ord2 9763 r1pwss 9766 rankwflemb 9775 r1elwf 9778 r1elssi 9787 uniwf 9801 itunitc1 10422 wunelss 10711 tskr1om2 10771 tskuni 10786 tskurn 10792 gruelss 10797 tz9.1regs 35571 dfon2lem6 36299 dfon2lem9 36302 nmuladdss 36726 axtco2g 37029 tr0elw 37036 tr0el 37037 ttctr2 37046 ttciunun 37063 setindtr 43792 dford3lem1 43794 ordelordALT 45287 trsspwALT 45567 trsspwALT2 45568 trsspwALT3 45569 pwtrVD 45573 ordelordALTVD 45616 ralabso 45718 rexabso 45719 modelaxrep 45731 omelaxinf2 45739 |
| Copyright terms: Public domain | W3C validator |