Theorem elpr 4626

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2108  Vcvv 3459  {cpr 4603

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  difprsnss  4775  preq12b  4826  pwpr  4877  pwtp  4878  uniprg  4899  intprg  4957  axprALT  5392  zfpair2  5403  opthwiener  5489  tpres  7192  fnprb  7199  2oconcl  8513  pw2f1olem  9088  djuunxp  9933  sdom2en01  10314  gruun  10818  fzpr  13594  m1expeven  14125  bpoly2  16071  bpoly3  16072  lcmfpr  16644  isprm2  16699  gsumpr  19934  drngnidl  21202  psgninv  21540  psgnodpm  21546  mdetunilem7  22554  indistopon  22937  dfconn2  23355  cnconn  23358  unconn  23365  txindis  23570  txconn  23625  filconn  23819  xpsdsval  24318  rolle  25944  dvivthlem1  25963  ang180lem3  26771  ang180lem4  26772  wilthlem2  27029  sqff1o  27142  ppiub  27165  lgslem1  27258  lgsdir2lem4  27289  lgsdir2lem5  27290  gausslemma2dlem0i  27325  2lgslem3  27365  2lgslem4  27367  nosgnn0  27620  structiedg0val  28947  usgrexmplef  29184  3vfriswmgrlem  30204  prodpr  32751  cycpm2tr  33076  drngmxidlr  33439  lmat22lem  33794  signslema  34540  circlemethhgt  34621  subfacp1lem1  35147  subfacp1lem4  35151  rankeq1o  36135  onsucconni  36401  topdifinfindis  37310  poimirlem9  37599  divrngidl  37998  isfldidl  38038  dihmeetlem2N  41264  wopprc  43001  pw2f1ocnv  43008  kelac2lem  43035  prclaxpr  44958  permaxpr  44983  rnmptpr  45149  cncfiooicclem1  45870  paireqne  47473  31prm  47559  lighneallem4  47572  upgrimpths  47870  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  usgrexmpl2trifr  47989  nn0sumshdiglem2  48550  2arwcatlem1  49387  2arwcatlem5  49391  2arwcat  49392  onsetreclem3  49466