Theorem elpr 4651

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

Syntax hints:   ↔ wb 205   ∨ wo 845   = wceq 1541   ∈ wcel 2106  Vcvv 3474  {cpr 4630

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631

This theorem is referenced by:  difprsnss  4802  preq12b  4851  pwpr  4902  pwtp  4903  uniprg  4925  uniprOLD  4927  intprg  4985  intprOLD  4987  axprALT  5420  zfpair2  5428  opthwiener  5514  tpres  7204  fnprb  7212  2oconcl  8505  pw2f1olem  9078  djuunxp  9918  sdom2en01  10299  gruun  10803  fzpr  13558  m1expeven  14077  bpoly2  16003  bpoly3  16004  lcmfpr  16566  isprm2  16621  gsumpr  19825  drngnidl  20860  psgninv  21141  psgnodpm  21147  mdetunilem7  22127  indistopon  22511  dfconn2  22930  cnconn  22933  unconn  22940  txindis  23145  txconn  23200  filconn  23394  xpsdsval  23894  rolle  25514  dvivthlem1  25532  ang180lem3  26323  ang180lem4  26324  wilthlem2  26580  sqff1o  26693  ppiub  26714  lgslem1  26807  lgsdir2lem4  26838  lgsdir2lem5  26839  gausslemma2dlem0i  26874  2lgslem3  26914  2lgslem4  26916  nosgnn0  27168  structiedg0val  28320  usgrexmplef  28554  3vfriswmgrlem  29568  prodpr  32070  cycpm2tr  32319  lmat22lem  32866  signslema  33642  circlemethhgt  33724  subfacp1lem1  34239  subfacp1lem4  34243  rankeq1o  35218  onsucconni  35414  topdifinfindis  36319  poimirlem9  36589  divrngidl  36988  isfldidl  37028  dihmeetlem2N  40262  wopprc  41857  pw2f1ocnv  41864  kelac2lem  41894  rnmptpr  43961  cncfiooicclem1  44694  paireqne  46264  31prm  46350  lighneallem4  46363  nn0sumshdiglem2  47392  onsetreclem3  47836