Theorem elpr 4590

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

Syntax hints:   ↔ wb 208   ∨ wo 843   = wceq 1537   ∈ wcel 2114  Vcvv 3494  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-pr 4570

This theorem is referenced by:  difprsnss  4732  preq12b  4781  pwpr  4832  pwtp  4833  unipr  4855  intpr  4909  axprALT  5323  zfpair2  5331  opthwiener  5404  tpres  6963  fnprb  6971  2oconcl  8128  pw2f1olem  8621  djuunxp  9350  sdom2en01  9724  gruun  10228  fzpr  12963  m1expeven  13477  bpoly2  15411  bpoly3  15412  lcmfpr  15971  isprm2  16026  gsumpr  19075  drngnidl  20002  psgninv  20726  psgnodpm  20732  mdetunilem7  21227  indistopon  21609  dfconn2  22027  cnconn  22030  unconn  22037  txindis  22242  txconn  22297  filconn  22491  xpsdsval  22991  rolle  24587  dvivthlem1  24605  ang180lem3  25389  ang180lem4  25390  wilthlem2  25646  sqff1o  25759  ppiub  25780  lgslem1  25873  lgsdir2lem4  25904  lgsdir2lem5  25905  gausslemma2dlem0i  25940  2lgslem3  25980  2lgslem4  25982  structiedg0val  26807  usgrexmplef  27041  3vfriswmgrlem  28056  prodpr  30542  cycpm2tr  30761  lmat22lem  31082  signslema  31832  circlemethhgt  31914  subfacp1lem1  32426  subfacp1lem4  32430  nosgnn0  33165  rankeq1o  33632  onsucconni  33785  topdifinfindis  34630  poimirlem9  34916  divrngidl  35321  isfldidl  35361  dihmeetlem2N  38450  wopprc  39676  pw2f1ocnv  39683  kelac2lem  39713  rnmptpr  41482  cncfiooicclem1  42225  paireqne  43722  31prm  43809  lighneallem4  43824  nn0sumshdiglem2  44731  onsetreclem3  44858