Theorem elpr 4610

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3444  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-sn 4586  df-pr 4588

This theorem is referenced by:  difprsnss  4759  preq12b  4810  pwpr  4861  pwtp  4862  uniprg  4883  intprg  4941  axprALT  5372  zfpair2  5383  opthwiener  5469  tpres  7157  fnprb  7164  2oconcl  8444  pw2f1olem  9022  djuunxp  9850  sdom2en01  10231  gruun  10735  fzpr  13516  m1expeven  14050  bpoly2  15999  bpoly3  16000  lcmfpr  16573  isprm2  16628  gsumpr  19869  drngnidl  21185  psgninv  21524  psgnodpm  21530  mdetunilem7  22538  indistopon  22921  dfconn2  23339  cnconn  23342  unconn  23349  txindis  23554  txconn  23609  filconn  23803  xpsdsval  24302  rolle  25927  dvivthlem1  25946  ang180lem3  26754  ang180lem4  26755  wilthlem2  27012  sqff1o  27125  ppiub  27148  lgslem1  27241  lgsdir2lem4  27272  lgsdir2lem5  27273  gausslemma2dlem0i  27308  2lgslem3  27348  2lgslem4  27350  nosgnn0  27603  structiedg0val  29002  usgrexmplef  29239  3vfriswmgrlem  30256  prodpr  32801  cycpm2tr  33091  drngmxidlr  33442  lmat22lem  33800  signslema  34546  circlemethhgt  34627  subfacp1lem1  35159  subfacp1lem4  35163  rankeq1o  36152  onsucconni  36418  topdifinfindis  37327  poimirlem9  37616  divrngidl  38015  isfldidl  38055  dihmeetlem2N  41286  wopprc  43012  pw2f1ocnv  43019  kelac2lem  43046  prclaxpr  44968  permaxpr  44993  rnmptpr  45164  cncfiooicclem1  45884  paireqne  47505  31prm  47591  lighneallem4  47604  upgrimpths  47902  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  pgnbgreunbgrlem3  48101  pgnbgreunbgrlem6  48107  nn0sumshdiglem2  48604  2arwcatlem1  49577  2arwcatlem5  49581  2arwcat  49582  onsetreclem3  49689