MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpr Structured version   Visualization version   GIF version

Theorem elpr 4582
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.)
Hypothesis
Ref Expression
elpr.1 𝐴 ∈ V
Assertion
Ref Expression
elpr (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))

Proof of Theorem elpr
StepHypRef Expression
1 elpr.1 . 2 𝐴 ∈ V
2 elprg 4580 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wo 843   = wceq 1530  wcel 2107  Vcvv 3493  {cpr 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-un 3939  df-sn 4560  df-pr 4562
This theorem is referenced by:  difprsnss  4724  preq12b  4773  pwpr  4824  pwtp  4825  unipr  4843  intpr  4900  axprALT  5313  zfpair2  5321  opthwiener  5395  tpres  6956  fnprb  6963  2oconcl  8120  pw2f1olem  8613  djuunxp  9342  sdom2en01  9716  gruun  10220  fzpr  12954  m1expeven  13468  bpoly2  15403  bpoly3  15404  lcmfpr  15963  isprm2  16018  gsumpr  19067  drngnidl  19994  psgninv  20718  psgnodpm  20724  mdetunilem7  21219  indistopon  21601  dfconn2  22019  cnconn  22022  unconn  22029  txindis  22234  txconn  22289  filconn  22483  xpsdsval  22983  rolle  24579  dvivthlem1  24597  ang180lem3  25381  ang180lem4  25382  wilthlem2  25638  sqff1o  25751  ppiub  25772  lgslem1  25865  lgsdir2lem4  25896  lgsdir2lem5  25897  gausslemma2dlem0i  25932  2lgslem3  25972  2lgslem4  25974  structiedg0val  26799  usgrexmplef  27033  3vfriswmgrlem  28048  prodpr  30535  cycpm2tr  30754  lmat22lem  31070  signslema  31820  circlemethhgt  31902  subfacp1lem1  32414  subfacp1lem4  32418  nosgnn0  33153  rankeq1o  33620  onsucconni  33773  topdifinfindis  34614  poimirlem9  34888  divrngidl  35293  isfldidl  35333  dihmeetlem2N  38422  wopprc  39612  pw2f1ocnv  39619  kelac2lem  39649  rnmptpr  41417  cncfiooicclem1  42160  paireqne  43658  31prm  43745  lighneallem4  43760  nn0sumshdiglem2  44667  onsetreclem3  44794
  Copyright terms: Public domain W3C validator