![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpr | Structured version Visualization version GIF version |
Description: A member of an unordered pair of classes is one or the other of them. 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 4418 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∨ wo 880 = wceq 1658 ∈ wcel 2166 Vcvv 3414 {cpr 4399 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-un 3803 df-sn 4398 df-pr 4400 |
This theorem is referenced by: difprsnss 4548 preq12b 4597 prel12OLD 4598 pwpr 4652 pwtp 4653 unipr 4671 intpr 4730 axpr 5126 zfpair2 5128 opthwiener 5200 tpres 6722 fnprb 6728 2oconcl 7850 pw2f1olem 8333 djuunxp 9060 sdom2en01 9439 gruun 9943 fzpr 12689 m1expeven 13201 bpoly2 15160 bpoly3 15161 lcmfpr 15713 isprm2 15767 drngnidl 19590 psgninv 20287 psgnodpm 20293 mdetunilem7 20792 indistopon 21176 dfconn2 21593 cnconn 21596 unconn 21603 txindis 21808 txconn 21863 filconn 22057 xpsdsval 22556 rolle 24152 dvivthlem1 24170 ang180lem3 24951 ang180lem4 24952 wilthlem2 25208 sqff1o 25321 ppiub 25342 lgslem1 25435 lgsdir2lem4 25466 lgsdir2lem5 25467 gausslemma2dlem0i 25502 2lgslem3 25542 2lgslem4 25544 structiedg0val 26320 usgrexmplef 26556 3vfriswmgrlem 27658 prodpr 30119 lmat22lem 30428 signslema 31186 circlemethhgt 31270 subfacp1lem1 31707 subfacp1lem4 31711 nosgnn0 32350 rankeq1o 32817 onsucconni 32969 topdifinfindis 33739 poimirlem9 33962 divrngidl 34369 isfldidl 34409 dihmeetlem2N 37374 wopprc 38440 pw2f1ocnv 38447 kelac2lem 38477 rnmptpr 40167 cncfiooicclem1 40901 31prm 42342 lighneallem4 42357 gsumpr 42986 nn0sumshdiglem2 43263 onsetreclem3 43348 |
Copyright terms: Public domain | W3C validator |