![]() |
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 4645 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 846 = wceq 1534 ∈ wcel 2099 Vcvv 3469 {cpr 4626 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-un 3949 df-sn 4625 df-pr 4627 |
This theorem is referenced by: difprsnss 4798 preq12b 4847 pwpr 4897 pwtp 4898 uniprg 4919 uniprOLD 4921 intprg 4979 intprOLD 4981 axprALT 5416 zfpair2 5424 opthwiener 5510 tpres 7207 fnprb 7214 2oconcl 8517 pw2f1olem 9092 djuunxp 9936 sdom2en01 10317 gruun 10821 fzpr 13580 m1expeven 14098 bpoly2 16025 bpoly3 16026 lcmfpr 16589 isprm2 16644 gsumpr 19901 drngnidl 21127 psgninv 21501 psgnodpm 21507 mdetunilem7 22507 indistopon 22891 dfconn2 23310 cnconn 23313 unconn 23320 txindis 23525 txconn 23580 filconn 23774 xpsdsval 24274 rolle 25909 dvivthlem1 25928 ang180lem3 26730 ang180lem4 26731 wilthlem2 26988 sqff1o 27101 ppiub 27124 lgslem1 27217 lgsdir2lem4 27248 lgsdir2lem5 27249 gausslemma2dlem0i 27284 2lgslem3 27324 2lgslem4 27326 nosgnn0 27578 structiedg0val 28822 usgrexmplef 29059 3vfriswmgrlem 30074 prodpr 32571 cycpm2tr 32818 lmat22lem 33354 signslema 34130 circlemethhgt 34211 subfacp1lem1 34725 subfacp1lem4 34729 rankeq1o 35703 onsucconni 35857 topdifinfindis 36761 poimirlem9 37037 divrngidl 37436 isfldidl 37476 dihmeetlem2N 40709 wopprc 42373 pw2f1ocnv 42380 kelac2lem 42410 rnmptpr 44473 cncfiooicclem1 45204 paireqne 46774 31prm 46860 lighneallem4 46873 nn0sumshdiglem2 47618 onsetreclem3 48061 |
Copyright terms: Public domain | W3C validator |