Theorem elpr 4655

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1537   ∈ wcel 2106  Vcvv 3478  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  difprsnss  4804  preq12b  4855  pwpr  4906  pwtp  4907  uniprg  4928  intprg  4986  axprALT  5428  zfpair2  5439  opthwiener  5524  tpres  7221  fnprb  7228  2oconcl  8540  pw2f1olem  9115  djuunxp  9959  sdom2en01  10340  gruun  10844  fzpr  13616  m1expeven  14147  bpoly2  16090  bpoly3  16091  lcmfpr  16661  isprm2  16716  gsumpr  19988  drngnidl  21271  psgninv  21618  psgnodpm  21624  mdetunilem7  22640  indistopon  23024  dfconn2  23443  cnconn  23446  unconn  23453  txindis  23658  txconn  23713  filconn  23907  xpsdsval  24407  rolle  26043  dvivthlem1  26062  ang180lem3  26869  ang180lem4  26870  wilthlem2  27127  sqff1o  27240  ppiub  27263  lgslem1  27356  lgsdir2lem4  27387  lgsdir2lem5  27388  gausslemma2dlem0i  27423  2lgslem3  27463  2lgslem4  27465  nosgnn0  27718  structiedg0val  29054  usgrexmplef  29291  3vfriswmgrlem  30306  prodpr  32833  cycpm2tr  33122  drngmxidlr  33486  lmat22lem  33778  signslema  34556  circlemethhgt  34637  subfacp1lem1  35164  subfacp1lem4  35168  rankeq1o  36153  onsucconni  36420  topdifinfindis  37329  poimirlem9  37616  divrngidl  38015  isfldidl  38055  dihmeetlem2N  41282  wopprc  43019  pw2f1ocnv  43026  kelac2lem  43053  prclaxpr  44948  rnmptpr  45120  cncfiooicclem1  45849  paireqne  47436  31prm  47522  lighneallem4  47535  usgrexmpl2nb1  47927  usgrexmpl2nb2  47928  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  usgrexmpl2trifr  47932  nn0sumshdiglem2  48472  onsetreclem3  48938