Theorem elpr 4548

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

Syntax hints:   ↔ wb 209   ∨ wo 844   = wceq 1538   ∈ wcel 2111  Vcvv 3441  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  difprsnss  4692  preq12b  4741  pwpr  4794  pwtp  4795  unipr  4817  intpr  4871  axprALT  5288  zfpair2  5296  opthwiener  5369  tpres  6940  fnprb  6948  2oconcl  8111  pw2f1olem  8604  djuunxp  9334  sdom2en01  9713  gruun  10217  fzpr  12957  m1expeven  13472  bpoly2  15403  bpoly3  15404  lcmfpr  15961  isprm2  16016  gsumpr  19068  drngnidl  19995  psgninv  20271  psgnodpm  20277  mdetunilem7  21223  indistopon  21606  dfconn2  22024  cnconn  22027  unconn  22034  txindis  22239  txconn  22294  filconn  22488  xpsdsval  22988  rolle  24593  dvivthlem1  24611  ang180lem3  25397  ang180lem4  25398  wilthlem2  25654  sqff1o  25767  ppiub  25788  lgslem1  25881  lgsdir2lem4  25912  lgsdir2lem5  25913  gausslemma2dlem0i  25948  2lgslem3  25988  2lgslem4  25990  structiedg0val  26815  usgrexmplef  27049  3vfriswmgrlem  28062  prodpr  30568  cycpm2tr  30811  lmat22lem  31170  signslema  31942  circlemethhgt  32024  subfacp1lem1  32539  subfacp1lem4  32543  nosgnn0  33278  rankeq1o  33745  onsucconni  33898  topdifinfindis  34763  poimirlem9  35066  divrngidl  35466  isfldidl  35506  dihmeetlem2N  38595  wopprc  39971  pw2f1ocnv  39978  kelac2lem  40008  rnmptpr  41801  cncfiooicclem1  42535  paireqne  44028  31prm  44114  lighneallem4  44128  nn0sumshdiglem2  45036  onsetreclem3  45236