Theorem elpr 4593

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

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

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 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  difprsnss  4743  preq12b  4794  pwpr  4845  pwtp  4846  uniprg  4867  intprg  4924  axprALT  5361  zfpair2  5373  prex  5377  opthwiener  5464  tpres  7151  fnprb  7158  2oconcl  8433  pw2f1olem  9014  djuunxp  9840  sdom2en01  10219  gruun  10724  fzpr  13528  m1expeven  14066  bpoly2  16017  bpoly3  16018  lcmfpr  16591  isprm2  16646  gsumpr  19925  drngnidl  21237  psgninv  21576  psgnodpm  21582  mdetunilem7  22597  indistopon  22980  dfconn2  23398  cnconn  23401  unconn  23408  txindis  23613  txconn  23668  filconn  23862  xpsdsval  24360  rolle  25971  dvivthlem1  25989  ang180lem3  26792  ang180lem4  26793  wilthlem2  27050  sqff1o  27163  ppiub  27185  lgslem1  27278  lgsdir2lem4  27309  lgsdir2lem5  27310  gausslemma2dlem0i  27345  2lgslem3  27385  2lgslem4  27387  nosgnn0  27640  structiedg0val  29109  usgrexmplef  29346  3vfriswmgrlem  30366  prodpr  32918  cycpm2tr  33199  drngmxidlr  33557  lmat22lem  33981  signslema  34726  circlemethhgt  34807  subfacp1lem1  35381  subfacp1lem4  35385  rankeq1o  36373  onsucconni  36639  topdifinfindis  37680  poimirlem9  37968  divrngidl  38367  isfldidl  38407  dihmeetlem2N  41763  wopprc  43480  pw2f1ocnv  43487  kelac2lem  43514  prclaxpr  45434  permaxpr  45459  rnmptpr  45629  cncfiooicclem1  46343  paireqne  47987  31prm  48076  lighneallem4  48089  upgrimpths  48401  usgrexmpl2nb1  48524  usgrexmpl2nb2  48525  usgrexmpl2nb4  48527  usgrexmpl2nb5  48528  usgrexmpl2trifr  48529  pgnbgreunbgrlem3  48610  pgnbgreunbgrlem6  48616  nn0sumshdiglem2  49114  2arwcatlem1  50086  2arwcatlem5  50090  2arwcat  50091  onsetreclem3  50198