Theorem elpr 4598

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

Step	Hyp	Ref	Expression
1		elpr.1	. 2 ⊢ 𝐴 ∈ V
2		elprg 4596	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {cpr 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576

This theorem is referenced by:  difprsnss  4748  preq12b  4799  pwpr  4850  pwtp  4851  uniprg  4872  intprg  4929  axprALT  5358  zfpair2  5369  opthwiener  5452  tpres  7135  fnprb  7142  2oconcl  8418  pw2f1olem  8994  djuunxp  9814  sdom2en01  10193  gruun  10697  fzpr  13479  m1expeven  14016  bpoly2  15964  bpoly3  15965  lcmfpr  16538  isprm2  16593  gsumpr  19867  drngnidl  21180  psgninv  21519  psgnodpm  21525  mdetunilem7  22533  indistopon  22916  dfconn2  23334  cnconn  23337  unconn  23344  txindis  23549  txconn  23604  filconn  23798  xpsdsval  24296  rolle  25921  dvivthlem1  25940  ang180lem3  26748  ang180lem4  26749  wilthlem2  27006  sqff1o  27119  ppiub  27142  lgslem1  27235  lgsdir2lem4  27266  lgsdir2lem5  27267  gausslemma2dlem0i  27302  2lgslem3  27342  2lgslem4  27344  nosgnn0  27597  structiedg0val  29000  usgrexmplef  29237  3vfriswmgrlem  30257  prodpr  32809  cycpm2tr  33088  drngmxidlr  33443  lmat22lem  33830  signslema  34575  circlemethhgt  34656  subfacp1lem1  35223  subfacp1lem4  35227  rankeq1o  36215  onsucconni  36481  topdifinfindis  37390  poimirlem9  37679  divrngidl  38078  isfldidl  38118  dihmeetlem2N  41408  wopprc  43133  pw2f1ocnv  43140  kelac2lem  43167  prclaxpr  45088  permaxpr  45113  rnmptpr  45284  cncfiooicclem1  46001  paireqne  47621  31prm  47707  lighneallem4  47720  upgrimpths  48019  usgrexmpl2nb1  48142  usgrexmpl2nb2  48143  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146  usgrexmpl2trifr  48147  pgnbgreunbgrlem3  48228  pgnbgreunbgrlem6  48234  nn0sumshdiglem2  48733  2arwcatlem1  49706  2arwcatlem5  49710  2arwcat  49711  onsetreclem3  49818