![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eltp | Structured version Visualization version GIF version |
Description: A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Ref | Expression |
---|---|
eltp.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
eltp | ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eltp.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | eltpg 4651 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ w3o 1087 = wceq 1542 ∈ wcel 2107 Vcvv 3448 {ctp 4595 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-un 3920 df-sn 4592 df-pr 4594 df-tp 4596 |
This theorem is referenced by: dftp2 4655 tpid1 4734 tpid2 4736 brtp 5485 tpres 7155 fntpb 7164 bpoly3 15948 cnfldfun 20824 gausslemma2dlem0i 26728 2lgsoddprm 26780 sltsolem1 27039 nb3grprlem1 28370 frgr3vlem1 29259 frgr3vlem2 29260 prodtp 31765 s3f1 31845 hgt750lemb 33309 fmtno4prmfac 45838 |
Copyright terms: Public domain | W3C validator |