| 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 4686 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∨ w3o 1086 = wceq 1540 ∈ wcel 2108 Vcvv 3480 {ctp 4630 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-sn 4627 df-pr 4629 df-tp 4631 |
| This theorem is referenced by: dftp2 4691 tpid1 4768 tpid2 4770 brtp 5528 tpres 7221 fntpb 7229 bpoly3 16094 cnfldfun 21378 cnfldfunOLD 21391 gausslemma2dlem0i 27408 2lgsoddprm 27460 sltsolem1 27720 nb3grprlem1 29397 frgr3vlem1 30292 frgr3vlem2 30293 prodtp 32829 s3f1 32931 hgt750lemb 34671 fmtno4prmfac 47559 usgrexmpl2nb0 47990 usgrexmpl2nb3 47993 usgrexmpl2trifr 47996 gpgnbgrvtx0 48030 gpgnbgrvtx1 48031 |
| Copyright terms: Public domain | W3C validator |