Theorem elpr 4146

Description: A member of an unordered pair of classes is one or the other of them. 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 4144	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   ↔ wb 195   ∨ wo 382   = wceq 1475   ∈ wcel 1977  Vcvv 3173  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  difprsnss  4270  preqr1OLD  4320  preq12b  4322  prel12  4323  pwpr  4368  pwtp  4369  unipr  4385  intpr  4445  axpr  4832  zfpair2  4834  elopOLD  4863  opthwiener  4901  tpres  6371  fnprb  6377  2oconcl  7470  pw2f1olem  7949  sdom2en01  9007  gruun  9507  fzpr  12266  m1expeven  12769  bpoly2  14627  bpoly3  14628  lcmfpr  15178  isprm2  15233  drngnidl  19050  psgninv  19747  psgnodpm  19753  mdetunilem7  20243  indistopon  20615  dfcon2  21032  cnconn  21035  uncon  21042  txindis  21247  txcon  21302  filcon  21497  xpsdsval  21996  rolle  23557  dvivthlem1  23575  ang180lem3  24341  ang180lem4  24342  wilthlem2  24595  sqff1o  24708  ppiub  24729  lgslem1  24822  lgsdir2lem4  24853  lgsdir2lem5  24854  gausslemma2dlem0i  24889  2lgslem3  24929  2lgslem4  24931  structiedg0val  25699  usgraexmplef  25929  3vfriswmgralem  26531  lmat22lem  29211  signslema  29965  subfacp1lem1  30415  subfacp1lem4  30419  nosgnn0  31055  rankeq1o  31448  onsucconi  31606  topdifinfindis  32370  poimirlem9  32588  divrngidl  32997  isfldidl  33037  dihmeetlem2N  35606  wopprc  36615  pw2f1ocnv  36622  kelac2lem  36652  rnmptpr  38353  cncfiooicclem1  38779  31prm  40050  lighneallem4  40065  3vfriswmgrlem  41447  gsumpr  41932  nn0sumshdiglem2  42214  onsetreclem3  42249