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

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

Proof of Theorem elpr
StepHypRef Expression
1 elpr.1 . 2 𝐴 ∈ V
2 elprg 4612 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
31, 2ax-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