Theorem elpr 4672

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

Syntax hints:   ↔ wb 206   ∨ wo 846   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  difprsnss  4824  preq12b  4875  pwpr  4925  pwtp  4926  uniprg  4947  intprg  5005  axprALT  5440  zfpair2  5448  opthwiener  5533  tpres  7238  fnprb  7245  2oconcl  8559  pw2f1olem  9142  djuunxp  9990  sdom2en01  10371  gruun  10875  fzpr  13639  m1expeven  14160  bpoly2  16105  bpoly3  16106  lcmfpr  16674  isprm2  16729  gsumpr  19997  drngnidl  21276  psgninv  21623  psgnodpm  21629  mdetunilem7  22645  indistopon  23029  dfconn2  23448  cnconn  23451  unconn  23458  txindis  23663  txconn  23718  filconn  23912  xpsdsval  24412  rolle  26048  dvivthlem1  26067  ang180lem3  26872  ang180lem4  26873  wilthlem2  27130  sqff1o  27243  ppiub  27266  lgslem1  27359  lgsdir2lem4  27390  lgsdir2lem5  27391  gausslemma2dlem0i  27426  2lgslem3  27466  2lgslem4  27468  nosgnn0  27721  structiedg0val  29057  usgrexmplef  29294  3vfriswmgrlem  30309  prodpr  32830  cycpm2tr  33112  drngmxidlr  33471  lmat22lem  33763  signslema  34539  circlemethhgt  34620  subfacp1lem1  35147  subfacp1lem4  35151  rankeq1o  36135  onsucconni  36403  topdifinfindis  37312  poimirlem9  37589  divrngidl  37988  isfldidl  38028  dihmeetlem2N  41256  wopprc  42987  pw2f1ocnv  42994  kelac2lem  43021  rnmptpr  45084  cncfiooicclem1  45814  paireqne  47385  31prm  47471  lighneallem4  47484  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  nn0sumshdiglem2  48356  onsetreclem3  48799