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 207   ∨ wo 853   = wceq 1547   ∈ wcel 2119  Vcvv 3431  {cpr 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4557  df-pr 4559

This theorem is referenced by:  difprsnss  4733  preq12b  4782  pwpr  4833  pwtp  4834  uniprg  4855  intprg  4912  axprALT  5352  zfpair2  5364  prex  5368  opthwiener  5456  tpres  7146  fnprb  7153  2oconcl  8429  pw2f1olem  9010  djuunxp  9837  sdom2en01  10216  gruun  10721  fzpr  13525  m1expeven  14063  bpoly2  16014  bpoly3  16015  lcmfpr  16588  isprm2  16643  gsumpr  19922  drngnidl  21237  psgninv  21558  psgnodpm  21564  mdetunilem7  22602  indistopon  22985  dfconn2  23403  cnconn  23406  unconn  23413  txindis  23618  txconn  23673  filconn  23867  xpsdsval  24365  rolle  25976  dvivthlem1  25994  ang180lem3  26794  ang180lem4  26795  wilthlem2  27051  sqff1o  27164  ppiub  27186  lgslem1  27279  lgsdir2lem4  27310  lgsdir2lem5  27311  gausslemma2dlem0i  27346  2lgslem3  27386  2lgslem4  27388  nosgnn0  27641  structiedg0val  29110  usgrexmplef  29347  3vfriswmgrlem  30366  prodpr  32919  cycpm2tr  33201  drngmxidlr  33562  lmat22lem  34010  signslema  34755  circlemethhgt  34836  subfacp1lem1  35416  subfacp1lem4  35420  rankeq1o  36408  onsucconni  36674  topdifinfindis  37717  poimirlem9  38005  divrngidl  38404  isfldidl  38444  dihmeetlem2N  41800  wopprc  43484  pw2f1ocnv  43491  kelac2lem  43518  prclaxpr  45438  permaxpr  45463  rnmptpr  45632  cncfiooicclem1  46344  paireqne  47994  31prm  48083  lighneallem4  48096  upgrimpths  48408  usgrexmpl2nb1  48531  usgrexmpl2nb2  48532  usgrexmpl2nb4  48534  usgrexmpl2nb5  48535  usgrexmpl2trifr  48536  pgnbgreunbgrlem3  48617  pgnbgreunbgrlem6  48623  nn0sumshdiglem2  49121  2arwcatlem1  50093  2arwcatlem5  50097  2arwcat  50098  onsetreclem3  50205