![]() |
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 | df-ss 3980 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) | |
2 | df-tr 5266 | . 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | |
3 | 19.23v 1940 | . . . 4 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | |
4 | eluni 4915 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
5 | 4 | imbi1i 349 | . . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
6 | 3, 5 | bitr4i 278 | . . 3 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) |
7 | 6 | albii 1816 | . 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) |
8 | 1, 2, 7 | 3bitr4i 303 | 1 ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1535 ∃wex 1776 ∈ wcel 2106 ⊆ wss 3963 ∪ cuni 4912 Tr wtr 5265 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-ss 3980 df-uni 4913 df-tr 5266 |
This theorem is referenced by: dftr2c 5268 dftr5OLD 5270 trel 5274 ordelord 6408 suctr 6472 trom 7896 hartogs 9582 card2on 9592 trcl 9766 tskwe 9988 ondomon 10601 nosupno 27763 noinfno 27778 dftr6 35731 elpotr 35763 hftr 36164 dford4 43018 mnutrd 44276 tratrb 44534 trsbc 44538 truniALT 44539 sspwtr 44819 sspwtrALT 44820 sspwtrALT2 44821 pwtrVD 44822 pwtrrVD 44823 suctrALT 44824 suctrALT2VD 44834 suctrALT2 44835 tratrbVD 44859 trsbcVD 44875 truniALTVD 44876 trintALTVD 44878 trintALT 44879 suctrALTcf 44920 suctrALTcfVD 44921 suctrALT3 44922 |
Copyright terms: Public domain | W3C validator |