Theorem elpr 4609

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1569   ∈ wcel 2146  Vcvv 3454  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  difprsnss  4762  preq12b  4808  pwpr  4831  pwtp  4832  uniprg  4886  intprg  4944  axprALT  5388  zfpair2  5396  prex  5400  opthwiener  5491  tpres  7217  fnprb  7224  2oconcl  8525  pw2f1olem  9114  djuunxp  10015  sdom2en01  10393  gruun  10904  fzpr  13726  m1expeven  14265  bpoly2  16238  bpoly3  16239  lcmfpr  16817  isprm2  16872  gsumpr  20184  drngnidl  21546  psgninv  21903  psgnodpm  21909  mdetunilem7  22948  indistopon  23334  dfconn2  23752  cnconn  23755  unconn  23762  txindis  23968  txconn  24023  filconn  24217  xpsdsval  24715  rolle  26325  dvivthlem1  26343  ang180lem3  27154  ang180lem4  27155  wilthlem2  27411  sqff1o  27524  ppiub  27546  lgslem1  27639  lgsdir2lem4  27670  lgsdir2lem5  27671  gausslemma2dlem0i  27706  2lgslem3  27746  2lgslem4  27748  nosgnn0  28030  structiedg0val  29615  usgrexmplef  29855  3vfriswmgrlem  30893  prodpr  33473  cycpm2tr  33736  drngmxidlr  34058  lmat22lem  34505  signslema  35247  circlemethhgt  35328  subfacp1lem1  36068  subfacp1lem4  36072  rankeq1o  37062  onsucconni  37355  topdifinfindis  38412  poimirlem9  38690  impprop  38787  divrngidl  39105  isfldidl  39145  dihmeetlem2N  42499  wopprc  44180  pw2f1ocnv  44187  kelac2lem  44209  prclaxpr  46117  permaxpr  46142  rnmptpr  46334  cncfiooicclem1  47045  paireqne  48735  31prm  48824  lighneallem4  48837  upgrimpths  49149  usgrexmpl2nb1  49272  usgrexmpl2nb2  49273  usgrexmpl2nb4  49275  usgrexmpl2nb5  49276  usgrexmpl2trifr  49277  pgnbgreunbgrlem3  49358  pgnbgreunbgrlem6  49364  nn0sumshdiglem2  49876  2arwcatlem1  50875  2arwcatlem5  50879  2arwcat  50880  onsetreclem3  51017