Theorem elpr 4545

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

Syntax hints:   ↔ wb 209   ∨ wo 844   = wceq 1538   ∈ wcel 2111  Vcvv 3409  {cpr 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-sn 4523  df-pr 4525

This theorem is referenced by:  difprsnss  4689  preq12b  4738  pwpr  4792  pwtp  4793  uniprg  4815  uniprOLD  4817  intprg  4871  intprOLD  4873  axprALT  5291  zfpair2  5299  opthwiener  5373  tpres  6954  fnprb  6962  2oconcl  8138  pw2f1olem  8642  djuunxp  9383  sdom2en01  9762  gruun  10266  fzpr  13011  m1expeven  13526  bpoly2  15459  bpoly3  15460  lcmfpr  16023  isprm2  16078  gsumpr  19143  drngnidl  20070  psgninv  20347  psgnodpm  20353  mdetunilem7  21318  indistopon  21701  dfconn2  22119  cnconn  22122  unconn  22129  txindis  22334  txconn  22389  filconn  22583  xpsdsval  23083  rolle  24689  dvivthlem1  24707  ang180lem3  25496  ang180lem4  25497  wilthlem2  25753  sqff1o  25866  ppiub  25887  lgslem1  25980  lgsdir2lem4  26011  lgsdir2lem5  26012  gausslemma2dlem0i  26047  2lgslem3  26087  2lgslem4  26089  structiedg0val  26914  usgrexmplef  27148  3vfriswmgrlem  28161  prodpr  30664  cycpm2tr  30912  lmat22lem  31288  signslema  32060  circlemethhgt  32142  subfacp1lem1  32657  subfacp1lem4  32661  nosgnn0  33426  rankeq1o  34022  onsucconni  34175  topdifinfindis  35043  poimirlem9  35346  divrngidl  35746  isfldidl  35786  dihmeetlem2N  38875  wopprc  40344  pw2f1ocnv  40351  kelac2lem  40381  rnmptpr  42172  cncfiooicclem1  42901  paireqne  44396  31prm  44482  lighneallem4  44495  nn0sumshdiglem2  45401  onsetreclem3  45627