Theorem elpr 4581

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

Syntax hints:   ↔ wb 205   ∨ wo 843   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  difprsnss  4729  preq12b  4778  pwpr  4830  pwtp  4831  uniprg  4853  uniprOLD  4855  intprg  4909  intprOLD  4911  axprALT  5340  zfpair2  5348  opthwiener  5422  tpres  7058  fnprb  7066  2oconcl  8295  pw2f1olem  8816  djuunxp  9610  sdom2en01  9989  gruun  10493  fzpr  13240  m1expeven  13758  bpoly2  15695  bpoly3  15696  lcmfpr  16260  isprm2  16315  gsumpr  19471  drngnidl  20413  psgninv  20699  psgnodpm  20705  mdetunilem7  21675  indistopon  22059  dfconn2  22478  cnconn  22481  unconn  22488  txindis  22693  txconn  22748  filconn  22942  xpsdsval  23442  rolle  25059  dvivthlem1  25077  ang180lem3  25866  ang180lem4  25867  wilthlem2  26123  sqff1o  26236  ppiub  26257  lgslem1  26350  lgsdir2lem4  26381  lgsdir2lem5  26382  gausslemma2dlem0i  26417  2lgslem3  26457  2lgslem4  26459  structiedg0val  27295  usgrexmplef  27529  3vfriswmgrlem  28542  prodpr  31042  cycpm2tr  31288  lmat22lem  31669  signslema  32441  circlemethhgt  32523  subfacp1lem1  33041  subfacp1lem4  33045  nosgnn0  33788  rankeq1o  34400  onsucconni  34553  topdifinfindis  35444  poimirlem9  35713  divrngidl  36113  isfldidl  36153  dihmeetlem2N  39240  wopprc  40768  pw2f1ocnv  40775  kelac2lem  40805  rnmptpr  42602  cncfiooicclem1  43324  paireqne  44851  31prm  44937  lighneallem4  44950  nn0sumshdiglem2  45856  onsetreclem3  46298