| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elpr | Structured version Visualization version GIF version | ||
| Description: A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
| Ref | Expression |
|---|---|
| elpr.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| elpr | ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elpr.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | elprg 4648 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∨ wo 848 = wceq 1540 ∈ wcel 2108 Vcvv 3480 {cpr 4628 |
| 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-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 |
| This theorem is referenced by: difprsnss 4799 preq12b 4850 pwpr 4901 pwtp 4902 uniprg 4923 intprg 4981 axprALT 5422 zfpair2 5433 opthwiener 5519 tpres 7221 fnprb 7228 2oconcl 8541 pw2f1olem 9116 djuunxp 9961 sdom2en01 10342 gruun 10846 fzpr 13619 m1expeven 14150 bpoly2 16093 bpoly3 16094 lcmfpr 16664 isprm2 16719 gsumpr 19973 drngnidl 21253 psgninv 21600 psgnodpm 21606 mdetunilem7 22624 indistopon 23008 dfconn2 23427 cnconn 23430 unconn 23437 txindis 23642 txconn 23697 filconn 23891 xpsdsval 24391 rolle 26028 dvivthlem1 26047 ang180lem3 26854 ang180lem4 26855 wilthlem2 27112 sqff1o 27225 ppiub 27248 lgslem1 27341 lgsdir2lem4 27372 lgsdir2lem5 27373 gausslemma2dlem0i 27408 2lgslem3 27448 2lgslem4 27450 nosgnn0 27703 structiedg0val 29039 usgrexmplef 29276 3vfriswmgrlem 30296 prodpr 32828 cycpm2tr 33139 drngmxidlr 33506 lmat22lem 33816 signslema 34577 circlemethhgt 34658 subfacp1lem1 35184 subfacp1lem4 35188 rankeq1o 36172 onsucconni 36438 topdifinfindis 37347 poimirlem9 37636 divrngidl 38035 isfldidl 38075 dihmeetlem2N 41301 wopprc 43042 pw2f1ocnv 43049 kelac2lem 43076 prclaxpr 45002 rnmptpr 45182 cncfiooicclem1 45908 paireqne 47498 31prm 47584 lighneallem4 47597 usgrexmpl2nb1 47991 usgrexmpl2nb2 47992 usgrexmpl2nb4 47994 usgrexmpl2nb5 47995 usgrexmpl2trifr 47996 nn0sumshdiglem2 48543 onsetreclem3 49226 |
| Copyright terms: Public domain | W3C validator |