Theorem elpr 4584

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

Syntax hints:   ↔ wb 208   ∨ wo 843   = wceq 1533   ∈ wcel 2110  Vcvv 3495  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3941  df-sn 4562  df-pr 4564

This theorem is referenced by:  difprsnss  4726  preq12b  4775  pwpr  4826  pwtp  4827  unipr  4845  intpr  4902  axprALT  5315  zfpair2  5323  opthwiener  5397  tpres  6958  fnprb  6965  2oconcl  8122  pw2f1olem  8615  djuunxp  9344  sdom2en01  9718  gruun  10222  fzpr  12956  m1expeven  13470  bpoly2  15405  bpoly3  15406  lcmfpr  15965  isprm2  16020  gsumpr  19069  drngnidl  19996  psgninv  20720  psgnodpm  20726  mdetunilem7  21221  indistopon  21603  dfconn2  22021  cnconn  22024  unconn  22031  txindis  22236  txconn  22291  filconn  22485  xpsdsval  22985  rolle  24581  dvivthlem1  24599  ang180lem3  25383  ang180lem4  25384  wilthlem2  25640  sqff1o  25753  ppiub  25774  lgslem1  25867  lgsdir2lem4  25898  lgsdir2lem5  25899  gausslemma2dlem0i  25934  2lgslem3  25974  2lgslem4  25976  structiedg0val  26801  usgrexmplef  27035  3vfriswmgrlem  28050  prodpr  30537  cycpm2tr  30756  lmat22lem  31077  signslema  31827  circlemethhgt  31909  subfacp1lem1  32421  subfacp1lem4  32425  nosgnn0  33160  rankeq1o  33627  onsucconni  33780  topdifinfindis  34621  poimirlem9  34895  divrngidl  35300  isfldidl  35340  dihmeetlem2N  38429  wopprc  39620  pw2f1ocnv  39627  kelac2lem  39657  rnmptpr  41425  cncfiooicclem1  42168  paireqne  43666  31prm  43753  lighneallem4  43768  nn0sumshdiglem2  44675  onsetreclem3  44802