Theorem elpr 4619

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

Syntax hints:   ↔ wb 209   ∨ wo 860   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  difprsnss  4771  preq12b  4819  pwpr  4870  pwtp  4871  uniprg  4892  intprg  4950  axprALT  5394  zfpair2  5406  prex  5410  opthwiener  5498  tpres  7200  fnprb  7207  2oconcl  8488  pw2f1olem  9069  djuunxp  9907  sdom2en01  10286  gruun  10791  fzpr  13607  m1expeven  14145  bpoly2  16111  bpoly3  16112  lcmfpr  16685  isprm2  16740  gsumpr  20025  drngnidl  21351  psgninv  21701  psgnodpm  21707  mdetunilem7  22744  indistopon  23127  dfconn2  23545  cnconn  23548  unconn  23555  txindis  23760  txconn  23815  filconn  24009  xpsdsval  24507  rolle  26118  dvivthlem1  26136  ang180lem3  26942  ang180lem4  26943  wilthlem2  27199  sqff1o  27312  ppiub  27334  lgslem1  27427  lgsdir2lem4  27458  lgsdir2lem5  27459  gausslemma2dlem0i  27494  2lgslem3  27534  2lgslem4  27536  nosgnn0  27788  structiedg0val  29313  usgrexmplef  29550  3vfriswmgrlem  30569  prodpr  33111  cycpm2tr  33380  drngmxidlr  33705  lmat22lem  34152  signslema  34894  circlemethhgt  34975  subfacp1lem1  35604  subfacp1lem4  35608  rankeq1o  36596  onsucconni  36871  topdifinfindis  37914  poimirlem9  38202  divrngidl  38601  isfldidl  38641  dihmeetlem2N  41997  wopprc  43683  pw2f1ocnv  43690  kelac2lem  43717  prclaxpr  45620  permaxpr  45645  rnmptpr  45821  cncfiooicclem1  46533  paireqne  48183  31prm  48272  lighneallem4  48285  upgrimpths  48597  usgrexmpl2nb1  48720  usgrexmpl2nb2  48721  usgrexmpl2nb4  48723  usgrexmpl2nb5  48724  usgrexmpl2trifr  48725  pgnbgreunbgrlem3  48806  pgnbgreunbgrlem6  48812  nn0sumshdiglem2  49321  2arwcatlem1  50292  2arwcatlem5  50296  2arwcat  50297  onsetreclem3  50404