![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dftr3 | Structured version Visualization version GIF version |
Description: An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
Ref | Expression |
---|---|
dftr3 | ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dftr5 5263 | . 2 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) | |
2 | dfss3 3966 | . . 3 ⊢ (𝑥 ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) | |
3 | 2 | ralbii 3088 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) |
4 | 1, 3 | bitr4i 278 | 1 ⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2099 ∀wral 3056 ⊆ wss 3944 Tr wtr 5259 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3057 df-v 3471 df-in 3951 df-ss 3961 df-uni 4904 df-tr 5260 |
This theorem is referenced by: trss 5270 trin 5271 triun 5274 triin 5276 tron 6386 ssorduni 7775 sucexeloniOLD 7807 suceloniOLD 7809 dfrecs3 8386 dfrecs3OLD 8387 ordtypelem2 9536 tcwf 9900 itunitc 10438 wunex2 10755 wfgru 10833 nadd2rabtr 42785 |
Copyright terms: Public domain | W3C validator |