Theorem elpr 4608

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

Syntax hints:   ↔ wb 208   ∨ wo 858   = wceq 1561   ∈ wcel 2143  Vcvv 3455  {cpr 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4584  df-pr 4586

This theorem is referenced by:  difprsnss  4760  preq12b  4809  pwpr  4860  pwtp  4861  uniprg  4882  intprg  4940  axprALT  5380  zfpair2  5392  prex  5396  opthwiener  5484  tpres  7186  fnprb  7193  2oconcl  8473  pw2f1olem  9054  djuunxp  9880  sdom2en01  10260  gruun  10765  fzpr  13585  m1expeven  14123  bpoly2  16088  bpoly3  16089  lcmfpr  16662  isprm2  16717  gsumpr  19996  drngnidl  21314  psgninv  21635  psgnodpm  21641  mdetunilem7  22679  indistopon  23062  dfconn2  23480  cnconn  23483  unconn  23490  txindis  23695  txconn  23750  filconn  23944  xpsdsval  24442  rolle  26053  dvivthlem1  26071  ang180lem3  26877  ang180lem4  26878  wilthlem2  27134  sqff1o  27247  ppiub  27269  lgslem1  27362  lgsdir2lem4  27393  lgsdir2lem5  27394  gausslemma2dlem0i  27429  2lgslem3  27469  2lgslem4  27471  nosgnn0  27723  structiedg0val  29224  usgrexmplef  29461  3vfriswmgrlem  30480  prodpr  33029  cycpm2tr  33300  drngmxidlr  33667  lmat22lem  34115  signslema  34857  circlemethhgt  34938  subfacp1lem1  35530  subfacp1lem4  35534  rankeq1o  36522  onsucconni  36798  topdifinfindis  37841  poimirlem9  38129  divrngidl  38528  isfldidl  38568  dihmeetlem2N  41924  wopprc  43608  pw2f1ocnv  43615  kelac2lem  43642  prclaxpr  45562  permaxpr  45587  rnmptpr  45756  cncfiooicclem1  46468  paireqne  48118  31prm  48207  lighneallem4  48220  upgrimpths  48532  usgrexmpl2nb1  48655  usgrexmpl2nb2  48656  usgrexmpl2nb4  48658  usgrexmpl2nb5  48659  usgrexmpl2trifr  48660  pgnbgreunbgrlem3  48741  pgnbgreunbgrlem6  48747  nn0sumshdiglem2  49245  2arwcatlem1  50217  2arwcatlem5  50221  2arwcat  50222  onsetreclem3  50329