Theorem elpr 4592

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  difprsnss  4744  preq12b  4793  pwpr  4844  pwtp  4845  uniprg  4866  intprg  4923  axprALT  5364  zfpair2  5376  prex  5380  opthwiener  5468  tpres  7156  fnprb  7163  2oconcl  8438  pw2f1olem  9019  djuunxp  9845  sdom2en01  10224  gruun  10729  fzpr  13533  m1expeven  14071  bpoly2  16022  bpoly3  16023  lcmfpr  16596  isprm2  16651  gsumpr  19930  drngnidl  21241  psgninv  21562  psgnodpm  21568  mdetunilem7  22583  indistopon  22966  dfconn2  23384  cnconn  23387  unconn  23394  txindis  23599  txconn  23654  filconn  23848  xpsdsval  24346  rolle  25957  dvivthlem1  25975  ang180lem3  26775  ang180lem4  26776  wilthlem2  27032  sqff1o  27145  ppiub  27167  lgslem1  27260  lgsdir2lem4  27291  lgsdir2lem5  27292  gausslemma2dlem0i  27327  2lgslem3  27367  2lgslem4  27369  nosgnn0  27622  structiedg0val  29091  usgrexmplef  29328  3vfriswmgrlem  30347  prodpr  32899  cycpm2tr  33180  drngmxidlr  33538  lmat22lem  33961  signslema  34706  circlemethhgt  34787  subfacp1lem1  35361  subfacp1lem4  35365  rankeq1o  36353  onsucconni  36619  topdifinfindis  37662  poimirlem9  37950  divrngidl  38349  isfldidl  38389  dihmeetlem2N  41745  wopprc  43458  pw2f1ocnv  43465  kelac2lem  43492  prclaxpr  45412  permaxpr  45437  rnmptpr  45607  cncfiooicclem1  46321  paireqne  47971  31prm  48060  lighneallem4  48073  upgrimpths  48385  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  nn0sumshdiglem2  49098  2arwcatlem1  50070  2arwcatlem5  50074  2arwcat  50075  onsetreclem3  50182