Theorem elpr 4606

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

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3441  {cpr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-sn 4582  df-pr 4584

This theorem is referenced by:  difprsnss  4756  preq12b  4807  pwpr  4858  pwtp  4859  uniprg  4880  intprg  4937  axprALT  5368  zfpair2  5379  opthwiener  5463  tpres  7149  fnprb  7156  2oconcl  8432  pw2f1olem  9013  djuunxp  9837  sdom2en01  10216  gruun  10721  fzpr  13499  m1expeven  14036  bpoly2  15984  bpoly3  15985  lcmfpr  16558  isprm2  16613  gsumpr  19888  drngnidl  21202  psgninv  21541  psgnodpm  21547  mdetunilem7  22566  indistopon  22949  dfconn2  23367  cnconn  23370  unconn  23377  txindis  23582  txconn  23637  filconn  23831  xpsdsval  24329  rolle  25954  dvivthlem1  25973  ang180lem3  26781  ang180lem4  26782  wilthlem2  27039  sqff1o  27152  ppiub  27175  lgslem1  27268  lgsdir2lem4  27299  lgsdir2lem5  27300  gausslemma2dlem0i  27335  2lgslem3  27375  2lgslem4  27377  nosgnn0  27630  structiedg0val  29099  usgrexmplef  29336  3vfriswmgrlem  30356  prodpr  32909  cycpm2tr  33203  drngmxidlr  33561  lmat22lem  33976  signslema  34721  circlemethhgt  34802  subfacp1lem1  35375  subfacp1lem4  35379  rankeq1o  36367  onsucconni  36633  topdifinfindis  37553  poimirlem9  37832  divrngidl  38231  isfldidl  38271  dihmeetlem2N  41627  wopprc  43339  pw2f1ocnv  43346  kelac2lem  43373  prclaxpr  45293  permaxpr  45318  rnmptpr  45488  cncfiooicclem1  46204  paireqne  47824  31prm  47910  lighneallem4  47923  upgrimpths  48222  usgrexmpl2nb1  48345  usgrexmpl2nb2  48346  usgrexmpl2nb4  48348  usgrexmpl2nb5  48349  usgrexmpl2trifr  48350  pgnbgreunbgrlem3  48431  pgnbgreunbgrlem6  48437  nn0sumshdiglem2  48935  2arwcatlem1  49907  2arwcatlem5  49911  2arwcat  49912  onsetreclem3  50019