Theorem elpr 4617

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3450  {cpr 4594

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  difprsnss  4766  preq12b  4817  pwpr  4868  pwtp  4869  uniprg  4890  intprg  4948  axprALT  5380  zfpair2  5391  opthwiener  5477  tpres  7178  fnprb  7185  2oconcl  8470  pw2f1olem  9050  djuunxp  9881  sdom2en01  10262  gruun  10766  fzpr  13547  m1expeven  14081  bpoly2  16030  bpoly3  16031  lcmfpr  16604  isprm2  16659  gsumpr  19892  drngnidl  21160  psgninv  21498  psgnodpm  21504  mdetunilem7  22512  indistopon  22895  dfconn2  23313  cnconn  23316  unconn  23323  txindis  23528  txconn  23583  filconn  23777  xpsdsval  24276  rolle  25901  dvivthlem1  25920  ang180lem3  26728  ang180lem4  26729  wilthlem2  26986  sqff1o  27099  ppiub  27122  lgslem1  27215  lgsdir2lem4  27246  lgsdir2lem5  27247  gausslemma2dlem0i  27282  2lgslem3  27322  2lgslem4  27324  nosgnn0  27577  structiedg0val  28956  usgrexmplef  29193  3vfriswmgrlem  30213  prodpr  32758  cycpm2tr  33083  drngmxidlr  33456  lmat22lem  33814  signslema  34560  circlemethhgt  34641  subfacp1lem1  35173  subfacp1lem4  35177  rankeq1o  36166  onsucconni  36432  topdifinfindis  37341  poimirlem9  37630  divrngidl  38029  isfldidl  38069  dihmeetlem2N  41300  wopprc  43026  pw2f1ocnv  43033  kelac2lem  43060  prclaxpr  44982  permaxpr  45007  rnmptpr  45178  cncfiooicclem1  45898  paireqne  47516  31prm  47602  lighneallem4  47615  upgrimpths  47913  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  nn0sumshdiglem2  48615  2arwcatlem1  49588  2arwcatlem5  49592  2arwcat  49593  onsetreclem3  49700