Theorem elpr 4614

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 860   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {cpr 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592

This theorem is used by:  difprsnss  4767  preq12b  4815  pwpr  4866  pwtp  4867  uniprg  4888  intprg  4946  axprALT  5393  zfpair2  5405  prex  5409  opthwiener  5497  tpres  7199  fnprb  7206  2oconcl  8484  pw2f1olem  9065  djuunxp  9912  sdom2en01  10290  gruun  10795  fzpr  13612  m1expeven  14150  bpoly2  16115  bpoly3  16116  lcmfpr  16689  isprm2  16744  gsumpr  20029  drngnidl  21386  psgninv  21741  psgnodpm  21747  mdetunilem7  22784  indistopon  23167  dfconn2  23585  cnconn  23588  unconn  23595  txindis  23800  txconn  23855  filconn  24049  xpsdsval  24547  rolle  26158  dvivthlem1  26176  ang180lem3  26985  ang180lem4  26986  wilthlem2  27242  sqff1o  27355  ppiub  27377  lgslem1  27470  lgsdir2lem4  27501  lgsdir2lem5  27502  gausslemma2dlem0i  27537  2lgslem3  27577  2lgslem4  27579  nosgnn0  27831  structiedg0val  29381  usgrexmplef  29618  3vfriswmgrlem  30637  prodpr  33179  cycpm2tr  33448  drngmxidlr  33769  lmat22lem  34216  signslema  34958  circlemethhgt  35039  subfacp1lem1  35679  subfacp1lem4  35683  rankeq1o  36671  onsucconni  36976  topdifinfindis  38020  poimirlem9  38308  divrngidl  38707  isfldidl  38747  dihmeetlem2N  42101  wopprc  43785  pw2f1ocnv  43792  kelac2lem  43819  prclaxpr  45722  permaxpr  45747  rnmptpr  45923  cncfiooicclem1  46635  paireqne  48288  31prm  48377  lighneallem4  48390  upgrimpths  48702  usgrexmpl2nb1  48825  usgrexmpl2nb2  48826  usgrexmpl2nb4  48828  usgrexmpl2nb5  48829  usgrexmpl2trifr  48830  pgnbgreunbgrlem3  48911  pgnbgreunbgrlem6  48917  nn0sumshdiglem2  49430  2arwcatlem1  50401  2arwcatlem5  50405  2arwcat  50406  onsetreclem3  50513