|   | 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 5261 instead may avoid dependences on ax-11 2156. (Contributed by NM, 24-Apr-1994.) | 
| Ref | Expression | 
|---|---|
| dftr2 | ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-ss 3967 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) | |
| 2 | df-tr 5259 | . 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | |
| 3 | 19.23v 1941 | . . . 4 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | |
| 4 | eluni 4909 | . . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
| 5 | 4 | imbi1i 349 | . . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | 
| 6 | 3, 5 | bitr4i 278 | . . 3 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) | 
| 7 | 6 | albii 1818 | . 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴)) | 
| 8 | 1, 2, 7 | 3bitr4i 303 | 1 ⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1537 ∃wex 1778 ∈ wcel 2107 ⊆ wss 3950 ∪ cuni 4906 Tr wtr 5258 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-ss 3967 df-uni 4907 df-tr 5259 | 
| This theorem is referenced by: dftr2c 5261 dftr5OLD 5263 trel 5267 ordelord 6405 suctr 6469 trom 7897 hartogs 9585 card2on 9595 trcl 9769 tskwe 9991 ondomon 10604 nosupno 27749 noinfno 27764 dftr6 35752 elpotr 35783 hftr 36184 dford4 43046 mnutrd 44304 tratrb 44561 trsbc 44565 truniALT 44566 sspwtr 44846 sspwtrALT 44847 sspwtrALT2 44848 pwtrVD 44849 pwtrrVD 44850 suctrALT 44851 suctrALT2VD 44861 suctrALT2 44862 tratrbVD 44886 trsbcVD 44902 truniALTVD 44903 trintALTVD 44905 trintALT 44906 suctrALTcf 44947 suctrALTcfVD 44948 suctrALT3 44949 | 
| Copyright terms: Public domain | W3C validator |