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 5167 | . 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | |
2 | sseq1 3989 | . . 3 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) | |
3 | 2 | rspccv 3617 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | sylbi 218 | 1 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ∀wral 3135 ⊆ wss 3933 Tr wtr 5163 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-v 3494 df-in 3940 df-ss 3949 df-uni 4831 df-tr 5164 |
This theorem is referenced by: trin 5173 triun 5176 triin 5178 trintss 5180 tz7.2 5532 ordelss 6200 ordelord 6206 tz7.7 6210 trsucss 6269 omsinds 7589 tc2 9172 tcel 9175 r1ord3g 9196 r1ord2 9198 r1pwss 9201 rankwflemb 9210 r1elwf 9213 r1elssi 9222 uniwf 9236 itunitc1 9830 wunelss 10118 tskr1om2 10178 tskuni 10193 tskurn 10199 gruelss 10204 dfon2lem6 32930 dfon2lem9 32933 setindtr 39499 dford3lem1 39501 ordelordALT 40748 trsspwALT 41029 trsspwALT2 41030 trsspwALT3 41031 pwtrVD 41035 ordelordALTVD 41078 |
Copyright terms: Public domain | W3C validator |