Theorem elpr 4198

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

Syntax hints:   ↔ wb 196   ∨ wo 383   = wceq 1483   ∈ wcel 1990  Vcvv 3200  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  difprsnss  4329  preqr1OLD  4380  preq12b  4382  prel12  4383  pwpr  4430  pwtp  4431  unipr  4449  intpr  4510  axpr  4905  zfpair2  4907  elopOLD  4936  opthwiener  4976  tpres  6466  fnprb  6472  2oconcl  7583  pw2f1olem  8064  sdom2en01  9124  gruun  9628  fzpr  12396  m1expeven  12907  bpoly2  14788  bpoly3  14789  lcmfpr  15340  isprm2  15395  drngnidl  19229  psgninv  19928  psgnodpm  19934  mdetunilem7  20424  indistopon  20805  dfconn2  21222  cnconn  21225  unconn  21232  txindis  21437  txconn  21492  filconn  21687  xpsdsval  22186  rolle  23753  dvivthlem1  23771  ang180lem3  24541  ang180lem4  24542  wilthlem2  24795  sqff1o  24908  ppiub  24929  lgslem1  25022  lgsdir2lem4  25053  lgsdir2lem5  25054  gausslemma2dlem0i  25089  2lgslem3  25129  2lgslem4  25131  structiedg0val  25911  usgrexmplef  26151  3vfriswmgrlem  27141  prodpr  29572  lmat22lem  29883  signslema  30639  circlemethhgt  30721  subfacp1lem1  31161  subfacp1lem4  31165  nosgnn0  31811  rankeq1o  32278  onsucconni  32436  topdifinfindis  33194  poimirlem9  33418  divrngidl  33827  isfldidl  33867  dihmeetlem2N  36588  wopprc  37597  pw2f1ocnv  37604  kelac2lem  37634  rnmptpr  39358  cncfiooicclem1  40106  31prm  41512  lighneallem4  41527  gsumpr  42139  nn0sumshdiglem2  42416  onsetreclem3  42450