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 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

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

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 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  difprsnss  4763  preq12b  4814  pwpr  4865  pwtp  4866  uniprg  4887  intprg  4945  axprALT  5377  zfpair2  5388  opthwiener  5474  tpres  7175  fnprb  7182  2oconcl  8467  pw2f1olem  9045  djuunxp  9874  sdom2en01  10255  gruun  10759  fzpr  13540  m1expeven  14074  bpoly2  16023  bpoly3  16024  lcmfpr  16597  isprm2  16652  gsumpr  19885  drngnidl  21153  psgninv  21491  psgnodpm  21497  mdetunilem7  22505  indistopon  22888  dfconn2  23306  cnconn  23309  unconn  23316  txindis  23521  txconn  23576  filconn  23770  xpsdsval  24269  rolle  25894  dvivthlem1  25913  ang180lem3  26721  ang180lem4  26722  wilthlem2  26979  sqff1o  27092  ppiub  27115  lgslem1  27208  lgsdir2lem4  27239  lgsdir2lem5  27240  gausslemma2dlem0i  27275  2lgslem3  27315  2lgslem4  27317  nosgnn0  27570  structiedg0val  28949  usgrexmplef  29186  3vfriswmgrlem  30206  prodpr  32751  cycpm2tr  33076  drngmxidlr  33449  lmat22lem  33807  signslema  34553  circlemethhgt  34634  subfacp1lem1  35166  subfacp1lem4  35170  rankeq1o  36159  onsucconni  36425  topdifinfindis  37334  poimirlem9  37623  divrngidl  38022  isfldidl  38062  dihmeetlem2N  41293  wopprc  43019  pw2f1ocnv  43026  kelac2lem  43053  prclaxpr  44975  permaxpr  45000  rnmptpr  45171  cncfiooicclem1  45891  paireqne  47512  31prm  47598  lighneallem4  47611  upgrimpths  47909  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  nn0sumshdiglem2  48611  2arwcatlem1  49584  2arwcatlem5  49588  2arwcat  49589  onsetreclem3  49696