![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dftr2 | Structured version Visualization version GIF version |
Description: An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5268 instead may avoid dependences on ax-11 2155. (Contributed by NM, 24-Apr-1994.) |
Ref | Expression |
---|---|
dftr2 | ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 3968 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) | |
2 | df-tr 5266 | . 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | |
3 | 19.23v 1946 | . . . 4 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | |
4 | eluni 4911 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
5 | 4 | imbi1i 350 | . . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
6 | 3, 5 | bitr4i 278 | . . 3 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) |
7 | 6 | albii 1822 | . 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) |
8 | 1, 2, 7 | 3bitr4i 303 | 1 ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 ∃wex 1782 ∈ wcel 2107 ⊆ wss 3948 ∪ cuni 4908 Tr wtr 5265 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3955 df-ss 3965 df-uni 4909 df-tr 5266 |
This theorem is referenced by: dftr2c 5268 dftr5OLD 5270 trel 5274 ordelord 6384 suctr 6448 trom 7861 hartogs 9536 card2on 9546 trcl 9720 tskwe 9942 ondomon 10555 nosupno 27196 noinfno 27211 dftr6 34710 elpotr 34742 hftr 35143 dford4 41754 mnutrd 43025 tratrb 43283 trsbc 43287 truniALT 43288 sspwtr 43568 sspwtrALT 43569 sspwtrALT2 43570 pwtrVD 43571 pwtrrVD 43572 suctrALT 43573 suctrALT2VD 43583 suctrALT2 43584 tratrbVD 43608 trsbcVD 43624 truniALTVD 43625 trintALTVD 43627 trintALT 43628 suctrALTcf 43669 suctrALTcfVD 43670 suctrALT3 43671 |
Copyright terms: Public domain | W3C validator |