Theorem elpr 4647

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

Syntax hints:   ↔ wb 205   ∨ wo 846   = wceq 1534   ∈ wcel 2099  Vcvv 3469  {cpr 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-un 3949  df-sn 4625  df-pr 4627

This theorem is referenced by:  difprsnss  4798  preq12b  4847  pwpr  4897  pwtp  4898  uniprg  4919  uniprOLD  4921  intprg  4979  intprOLD  4981  axprALT  5416  zfpair2  5424  opthwiener  5510  tpres  7207  fnprb  7214  2oconcl  8517  pw2f1olem  9092  djuunxp  9936  sdom2en01  10317  gruun  10821  fzpr  13580  m1expeven  14098  bpoly2  16025  bpoly3  16026  lcmfpr  16589  isprm2  16644  gsumpr  19901  drngnidl  21127  psgninv  21501  psgnodpm  21507  mdetunilem7  22507  indistopon  22891  dfconn2  23310  cnconn  23313  unconn  23320  txindis  23525  txconn  23580  filconn  23774  xpsdsval  24274  rolle  25909  dvivthlem1  25928  ang180lem3  26730  ang180lem4  26731  wilthlem2  26988  sqff1o  27101  ppiub  27124  lgslem1  27217  lgsdir2lem4  27248  lgsdir2lem5  27249  gausslemma2dlem0i  27284  2lgslem3  27324  2lgslem4  27326  nosgnn0  27578  structiedg0val  28822  usgrexmplef  29059  3vfriswmgrlem  30074  prodpr  32571  cycpm2tr  32818  lmat22lem  33354  signslema  34130  circlemethhgt  34211  subfacp1lem1  34725  subfacp1lem4  34729  rankeq1o  35703  onsucconni  35857  topdifinfindis  36761  poimirlem9  37037  divrngidl  37436  isfldidl  37476  dihmeetlem2N  40709  wopprc  42373  pw2f1ocnv  42380  kelac2lem  42410  rnmptpr  44473  cncfiooicclem1  45204  paireqne  46774  31prm  46860  lighneallem4  46873  nn0sumshdiglem2  47618  onsetreclem3  48061