Theorem elpr 4602

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 4600	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3436  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-pr 4580

This theorem is referenced by:  difprsnss  4750  preq12b  4801  pwpr  4852  pwtp  4853  uniprg  4874  intprg  4931  axprALT  5361  zfpair2  5372  opthwiener  5457  tpres  7137  fnprb  7144  2oconcl  8421  pw2f1olem  8998  djuunxp  9817  sdom2en01  10196  gruun  10700  fzpr  13482  m1expeven  14016  bpoly2  15964  bpoly3  15965  lcmfpr  16538  isprm2  16593  gsumpr  19834  drngnidl  21150  psgninv  21489  psgnodpm  21495  mdetunilem7  22503  indistopon  22886  dfconn2  23304  cnconn  23307  unconn  23314  txindis  23519  txconn  23574  filconn  23768  xpsdsval  24267  rolle  25892  dvivthlem1  25911  ang180lem3  26719  ang180lem4  26720  wilthlem2  26977  sqff1o  27090  ppiub  27113  lgslem1  27206  lgsdir2lem4  27237  lgsdir2lem5  27238  gausslemma2dlem0i  27273  2lgslem3  27313  2lgslem4  27315  nosgnn0  27568  structiedg0val  28967  usgrexmplef  29204  3vfriswmgrlem  30221  prodpr  32772  cycpm2tr  33062  drngmxidlr  33416  lmat22lem  33790  signslema  34536  circlemethhgt  34617  subfacp1lem1  35162  subfacp1lem4  35166  rankeq1o  36155  onsucconni  36421  topdifinfindis  37330  poimirlem9  37619  divrngidl  38018  isfldidl  38058  dihmeetlem2N  41288  wopprc  43013  pw2f1ocnv  43020  kelac2lem  43047  prclaxpr  44969  permaxpr  44994  rnmptpr  45165  cncfiooicclem1  45884  paireqne  47505  31prm  47591  lighneallem4  47604  upgrimpths  47903  usgrexmpl2nb1  48026  usgrexmpl2nb2  48027  usgrexmpl2nb4  48029  usgrexmpl2nb5  48030  usgrexmpl2trifr  48031  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  nn0sumshdiglem2  48617  2arwcatlem1  49590  2arwcatlem5  49594  2arwcat  49595  onsetreclem3  49702