Theorem elpr 4584

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

Syntax hints:   ↔ wb 205   ∨ wo 844   = wceq 1539   ∈ wcel 2106  Vcvv 3432  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  difprsnss  4732  preq12b  4781  pwpr  4833  pwtp  4834  uniprg  4856  uniprOLD  4858  intprg  4912  intprOLD  4914  axprALT  5345  zfpair2  5353  opthwiener  5428  tpres  7076  fnprb  7084  2oconcl  8333  pw2f1olem  8863  djuunxp  9679  sdom2en01  10058  gruun  10562  fzpr  13311  m1expeven  13830  bpoly2  15767  bpoly3  15768  lcmfpr  16332  isprm2  16387  gsumpr  19556  drngnidl  20500  psgninv  20787  psgnodpm  20793  mdetunilem7  21767  indistopon  22151  dfconn2  22570  cnconn  22573  unconn  22580  txindis  22785  txconn  22840  filconn  23034  xpsdsval  23534  rolle  25154  dvivthlem1  25172  ang180lem3  25961  ang180lem4  25962  wilthlem2  26218  sqff1o  26331  ppiub  26352  lgslem1  26445  lgsdir2lem4  26476  lgsdir2lem5  26477  gausslemma2dlem0i  26512  2lgslem3  26552  2lgslem4  26554  structiedg0val  27392  usgrexmplef  27626  3vfriswmgrlem  28641  prodpr  31140  cycpm2tr  31386  lmat22lem  31767  signslema  32541  circlemethhgt  32623  subfacp1lem1  33141  subfacp1lem4  33145  nosgnn0  33861  rankeq1o  34473  onsucconni  34626  topdifinfindis  35517  poimirlem9  35786  divrngidl  36186  isfldidl  36226  dihmeetlem2N  39313  wopprc  40852  pw2f1ocnv  40859  kelac2lem  40889  rnmptpr  42713  cncfiooicclem1  43434  paireqne  44963  31prm  45049  lighneallem4  45062  nn0sumshdiglem2  45968  onsetreclem3  46412