![]() |
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 4612 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 846 = wceq 1542 ∈ wcel 2107 Vcvv 3448 {cpr 4593 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-un 3920 df-sn 4592 df-pr 4594 |
This theorem is referenced by: difprsnss 4764 preq12b 4813 pwpr 4864 pwtp 4865 uniprg 4887 uniprOLD 4889 intprg 4947 intprOLD 4949 axprALT 5382 zfpair2 5390 opthwiener 5476 tpres 7155 fnprb 7163 2oconcl 8454 pw2f1olem 9027 djuunxp 9864 sdom2en01 10245 gruun 10749 fzpr 13503 m1expeven 14022 bpoly2 15947 bpoly3 15948 lcmfpr 16510 isprm2 16565 gsumpr 19739 drngnidl 20715 psgninv 21002 psgnodpm 21008 mdetunilem7 21983 indistopon 22367 dfconn2 22786 cnconn 22789 unconn 22796 txindis 23001 txconn 23056 filconn 23250 xpsdsval 23750 rolle 25370 dvivthlem1 25388 ang180lem3 26177 ang180lem4 26178 wilthlem2 26434 sqff1o 26547 ppiub 26568 lgslem1 26661 lgsdir2lem4 26692 lgsdir2lem5 26693 gausslemma2dlem0i 26728 2lgslem3 26768 2lgslem4 26770 nosgnn0 27022 structiedg0val 28015 usgrexmplef 28249 3vfriswmgrlem 29263 prodpr 31764 cycpm2tr 32010 lmat22lem 32438 signslema 33214 circlemethhgt 33296 subfacp1lem1 33813 subfacp1lem4 33817 rankeq1o 34785 onsucconni 34938 topdifinfindis 35846 poimirlem9 36116 divrngidl 36516 isfldidl 36556 dihmeetlem2N 39791 wopprc 41383 pw2f1ocnv 41390 kelac2lem 41420 rnmptpr 43468 cncfiooicclem1 44208 paireqne 45777 31prm 45863 lighneallem4 45876 nn0sumshdiglem2 46782 onsetreclem3 47226 |
Copyright terms: Public domain | W3C validator |