Theorem elpr 4616

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2146  Vcvv 3457  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  difprsnss  4769  preq12b  4817  pwpr  4868  pwtp  4869  uniprg  4890  intprg  4948  axprALT  5395  zfpair2  5407  prex  5411  opthwiener  5499  tpres  7206  fnprb  7213  2oconcl  8494  pw2f1olem  9076  djuunxp  9923  sdom2en01  10301  gruun  10810  fzpr  13628  m1expeven  14167  bpoly2  16137  bpoly3  16138  lcmfpr  16711  isprm2  16766  gsumpr  20073  drngnidl  21431  psgninv  21786  psgnodpm  21792  mdetunilem7  22829  indistopon  23212  dfconn2  23630  cnconn  23633  unconn  23640  txindis  23846  txconn  23901  filconn  24095  xpsdsval  24593  rolle  26204  dvivthlem1  26222  ang180lem3  27031  ang180lem4  27032  wilthlem2  27288  sqff1o  27401  ppiub  27423  lgslem1  27516  lgsdir2lem4  27547  lgsdir2lem5  27548  gausslemma2dlem0i  27583  2lgslem3  27623  2lgslem4  27625  nosgnn0  27877  structiedg0val  29431  usgrexmplef  29671  3vfriswmgrlem  30703  prodpr  33244  cycpm2tr  33507  drngmxidlr  33828  lmat22lem  34275  signslema  35018  circlemethhgt  35099  subfacp1lem1  35712  subfacp1lem4  35716  rankeq1o  36704  onsucconni  37009  topdifinfindis  38053  poimirlem9  38341  divrngidl  38741  isfldidl  38781  dihmeetlem2N  42135  wopprc  43834  pw2f1ocnv  43841  kelac2lem  43868  prclaxpr  45771  permaxpr  45796  rnmptpr  45972  cncfiooicclem1  46684  paireqne  48337  31prm  48426  lighneallem4  48439  upgrimpths  48751  usgrexmpl2nb1  48874  usgrexmpl2nb2  48875  usgrexmpl2nb4  48877  usgrexmpl2nb5  48878  usgrexmpl2trifr  48879  pgnbgreunbgrlem3  48960  pgnbgreunbgrlem6  48966  nn0sumshdiglem2  49478  2arwcatlem1  50449  2arwcatlem5  50453  2arwcat  50454  onsetreclem3  50561