Theorem elpr 4609

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2145  Vcvv 3450  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  difprsnss  4762  preq12b  4810  pwpr  4861  pwtp  4862  uniprg  4883  intprg  4941  axprALT  5387  zfpair2  5399  prex  5403  opthwiener  5491  tpres  7201  fnprb  7208  2oconcl  8493  pw2f1olem  9082  djuunxp  9929  sdom2en01  10307  gruun  10818  fzpr  13637  m1expeven  14176  bpoly2  16146  bpoly3  16147  lcmfpr  16720  isprm2  16775  gsumpr  20085  drngnidl  21443  psgninv  21798  psgnodpm  21804  mdetunilem7  22843  indistopon  23229  dfconn2  23647  cnconn  23650  unconn  23657  txindis  23863  txconn  23918  filconn  24112  xpsdsval  24610  rolle  26220  dvivthlem1  26238  ang180lem3  27051  ang180lem4  27052  wilthlem2  27308  sqff1o  27421  ppiub  27443  lgslem1  27536  lgsdir2lem4  27567  lgsdir2lem5  27568  gausslemma2dlem0i  27603  2lgslem3  27643  2lgslem4  27645  nosgnn0  27897  structiedg0val  29482  usgrexmplef  29722  3vfriswmgrlem  30760  prodpr  33299  cycpm2tr  33562  drngmxidlr  33883  lmat22lem  34330  signslema  35073  circlemethhgt  35154  subfacp1lem1  35761  subfacp1lem4  35765  rankeq1o  36754  onsucconni  37059  topdifinfindis  38103  poimirlem9  38381  divrngidl  38781  isfldidl  38821  dihmeetlem2N  42175  wopprc  43874  pw2f1ocnv  43881  kelac2lem  43908  prclaxpr  45811  permaxpr  45836  rnmptpr  46012  cncfiooicclem1  46724  paireqne  48414  31prm  48503  lighneallem4  48516  upgrimpths  48828  usgrexmpl2nb1  48951  usgrexmpl2nb2  48952  usgrexmpl2nb4  48954  usgrexmpl2nb5  48955  usgrexmpl2trifr  48956  pgnbgreunbgrlem3  49037  pgnbgreunbgrlem6  49043  nn0sumshdiglem2  49555  2arwcatlem1  50524  2arwcatlem5  50528  2arwcat  50529  onsetreclem3  50636