Theorem elpr 4650

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

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1540   ∈ wcel 2108  Vcvv 3480  {cpr 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  difprsnss  4799  preq12b  4850  pwpr  4901  pwtp  4902  uniprg  4923  intprg  4981  axprALT  5422  zfpair2  5433  opthwiener  5519  tpres  7221  fnprb  7228  2oconcl  8541  pw2f1olem  9116  djuunxp  9961  sdom2en01  10342  gruun  10846  fzpr  13619  m1expeven  14150  bpoly2  16093  bpoly3  16094  lcmfpr  16664  isprm2  16719  gsumpr  19973  drngnidl  21253  psgninv  21600  psgnodpm  21606  mdetunilem7  22624  indistopon  23008  dfconn2  23427  cnconn  23430  unconn  23437  txindis  23642  txconn  23697  filconn  23891  xpsdsval  24391  rolle  26028  dvivthlem1  26047  ang180lem3  26854  ang180lem4  26855  wilthlem2  27112  sqff1o  27225  ppiub  27248  lgslem1  27341  lgsdir2lem4  27372  lgsdir2lem5  27373  gausslemma2dlem0i  27408  2lgslem3  27448  2lgslem4  27450  nosgnn0  27703  structiedg0val  29039  usgrexmplef  29276  3vfriswmgrlem  30296  prodpr  32828  cycpm2tr  33139  drngmxidlr  33506  lmat22lem  33816  signslema  34577  circlemethhgt  34658  subfacp1lem1  35184  subfacp1lem4  35188  rankeq1o  36172  onsucconni  36438  topdifinfindis  37347  poimirlem9  37636  divrngidl  38035  isfldidl  38075  dihmeetlem2N  41301  wopprc  43042  pw2f1ocnv  43049  kelac2lem  43076  prclaxpr  45002  rnmptpr  45182  cncfiooicclem1  45908  paireqne  47498  31prm  47584  lighneallem4  47597  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  nn0sumshdiglem2  48543  onsetreclem3  49226