Theorem elpr 4603

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {cpr 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-sn 4579  df-pr 4581

This theorem is referenced by:  difprsnss  4753  preq12b  4804  pwpr  4855  pwtp  4856  uniprg  4877  intprg  4934  axprALT  5365  zfpair2  5376  opthwiener  5460  tpres  7145  fnprb  7152  2oconcl  8428  pw2f1olem  9007  djuunxp  9831  sdom2en01  10210  gruun  10715  fzpr  13493  m1expeven  14030  bpoly2  15978  bpoly3  15979  lcmfpr  16552  isprm2  16607  gsumpr  19882  drngnidl  21196  psgninv  21535  psgnodpm  21541  mdetunilem7  22560  indistopon  22943  dfconn2  23361  cnconn  23364  unconn  23371  txindis  23576  txconn  23631  filconn  23825  xpsdsval  24323  rolle  25948  dvivthlem1  25967  ang180lem3  26775  ang180lem4  26776  wilthlem2  27033  sqff1o  27146  ppiub  27169  lgslem1  27262  lgsdir2lem4  27293  lgsdir2lem5  27294  gausslemma2dlem0i  27329  2lgslem3  27369  2lgslem4  27371  nosgnn0  27624  structiedg0val  29044  usgrexmplef  29281  3vfriswmgrlem  30301  prodpr  32856  cycpm2tr  33150  drngmxidlr  33508  lmat22lem  33923  signslema  34668  circlemethhgt  34749  subfacp1lem1  35322  subfacp1lem4  35326  rankeq1o  36314  onsucconni  36580  topdifinfindis  37490  poimirlem9  37769  divrngidl  38168  isfldidl  38208  dihmeetlem2N  41498  wopprc  43214  pw2f1ocnv  43221  kelac2lem  43248  prclaxpr  45168  permaxpr  45193  rnmptpr  45363  cncfiooicclem1  46079  paireqne  47699  31prm  47785  lighneallem4  47798  upgrimpths  48097  usgrexmpl2nb1  48220  usgrexmpl2nb2  48221  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  usgrexmpl2trifr  48225  pgnbgreunbgrlem3  48306  pgnbgreunbgrlem6  48312  nn0sumshdiglem2  48810  2arwcatlem1  49782  2arwcatlem5  49786  2arwcat  49787  onsetreclem3  49894