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  7193  fnprb  7200  2oconcl  8515  pw2f1olem  9090  djuunxp  9935  sdom2en01  10316  gruun  10820  fzpr  13596  m1expeven  14127  bpoly2  16073  bpoly3  16074  lcmfpr  16646  isprm2  16701  gsumpr  19936  drngnidl  21204  psgninv  21542  psgnodpm  21548  mdetunilem7  22556  indistopon  22939  dfconn2  23357  cnconn  23360  unconn  23367  txindis  23572  txconn  23627  filconn  23821  xpsdsval  24320  rolle  25946  dvivthlem1  25965  ang180lem3  26773  ang180lem4  26774  wilthlem2  27031  sqff1o  27144  ppiub  27167  lgslem1  27260  lgsdir2lem4  27291  lgsdir2lem5  27292  gausslemma2dlem0i  27327  2lgslem3  27367  2lgslem4  27369  nosgnn0  27622  structiedg0val  29001  usgrexmplef  29238  3vfriswmgrlem  30258  prodpr  32805  cycpm2tr  33130  drngmxidlr  33493  lmat22lem  33848  signslema  34594  circlemethhgt  34675  subfacp1lem1  35201  subfacp1lem4  35205  rankeq1o  36189  onsucconni  36455  topdifinfindis  37364  poimirlem9  37653  divrngidl  38052  isfldidl  38092  dihmeetlem2N  41318  wopprc  43054  pw2f1ocnv  43061  kelac2lem  43088  prclaxpr  45010  permaxpr  45035  rnmptpr  45201  cncfiooicclem1  45922  paireqne  47525  31prm  47611  lighneallem4  47624  upgrimpths  47922  usgrexmpl2nb1  48036  usgrexmpl2nb2  48037  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  usgrexmpl2trifr  48041  nn0sumshdiglem2  48602  2arwcatlem1  49472  2arwcatlem5  49476  2arwcat  49477  onsetreclem3  49571