![]() |
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 4690 | . 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 3475 {ctp 4633 |
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-or 847 df-3or 1089 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 df-sn 4630 df-pr 4632 df-tp 4634 |
This theorem is referenced by: dftp2 4694 tpid1 4773 tpid2 4775 brtp 5524 tpres 7202 fntpb 7211 bpoly3 16002 cnfldfun 20956 gausslemma2dlem0i 26867 2lgsoddprm 26919 sltsolem1 27178 nb3grprlem1 28637 frgr3vlem1 29526 frgr3vlem2 29527 prodtp 32033 s3f1 32113 hgt750lemb 33668 fmtno4prmfac 46240 |
Copyright terms: Public domain | W3C validator |