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

Theorem elpr 4189
 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 4187 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∨ wo 383   = wceq 1481   ∈ wcel 1988  Vcvv 3195  {cpr 4170 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572  df-sn 4169  df-pr 4171 This theorem is referenced by:  difprsnss  4320  preqr1OLD  4371  preq12b  4373  prel12  4374  pwpr  4421  pwtp  4422  unipr  4440  intpr  4501  axpr  4896  zfpair2  4898  elopOLD  4927  opthwiener  4966  tpres  6451  fnprb  6457  2oconcl  7568  pw2f1olem  8049  sdom2en01  9109  gruun  9613  fzpr  12381  m1expeven  12890  bpoly2  14769  bpoly3  14770  lcmfpr  15321  isprm2  15376  drngnidl  19210  psgninv  19909  psgnodpm  19915  mdetunilem7  20405  indistopon  20786  dfconn2  21203  cnconn  21206  unconn  21213  txindis  21418  txconn  21473  filconn  21668  xpsdsval  22167  rolle  23734  dvivthlem1  23752  ang180lem3  24522  ang180lem4  24523  wilthlem2  24776  sqff1o  24889  ppiub  24910  lgslem1  25003  lgsdir2lem4  25034  lgsdir2lem5  25035  gausslemma2dlem0i  25070  2lgslem3  25110  2lgslem4  25112  structiedg0val  25892  usgrexmplef  26132  3vfriswmgrlem  27121  prodpr  29546  lmat22lem  29857  signslema  30613  circlemethhgt  30695  subfacp1lem1  31135  subfacp1lem4  31139  nosgnn0  31785  rankeq1o  32253  onsucconni  32411  topdifinfindis  33165  poimirlem9  33389  divrngidl  33798  isfldidl  33838  dihmeetlem2N  36407  wopprc  37416  pw2f1ocnv  37423  kelac2lem  37453  rnmptpr  39174  cncfiooicclem1  39869  31prm  41277  lighneallem4  41292  gsumpr  41904  nn0sumshdiglem2  42181  onsetreclem3  42215
 Copyright terms: Public domain W3C validator