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 4587 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∨ w3o 1088 = wceq 1543 ∈ wcel 2112 Vcvv 3398 {ctp 4531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-un 3858 df-sn 4528 df-pr 4530 df-tp 4532 |
This theorem is referenced by: dftp2 4591 tpid1 4670 tpid2 4672 tpres 6994 fntpb 7003 bpoly3 15583 cnfldfunALT 20330 gausslemma2dlem0i 26199 2lgsoddprm 26251 nb3grprlem1 27422 frgr3vlem1 28310 frgr3vlem2 28311 prodtp 30815 s3f1 30895 hgt750lemb 32302 brtp 33386 sltsolem1 33564 fmtno4prmfac 44640 |
Copyright terms: Public domain | W3C validator |