Theorem elpr 4607

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

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {cpr 4584

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  difprsnss  4757  preq12b  4808  pwpr  4859  pwtp  4860  uniprg  4881  intprg  4938  axprALT  5371  zfpair2  5382  prex  5386  opthwiener  5472  tpres  7159  fnprb  7166  2oconcl  8442  pw2f1olem  9023  djuunxp  9847  sdom2en01  10226  gruun  10731  fzpr  13509  m1expeven  14046  bpoly2  15994  bpoly3  15995  lcmfpr  16568  isprm2  16623  gsumpr  19901  drngnidl  21215  psgninv  21554  psgnodpm  21560  mdetunilem7  22579  indistopon  22962  dfconn2  23380  cnconn  23383  unconn  23390  txindis  23595  txconn  23650  filconn  23844  xpsdsval  24342  rolle  25967  dvivthlem1  25986  ang180lem3  26794  ang180lem4  26795  wilthlem2  27052  sqff1o  27165  ppiub  27188  lgslem1  27281  lgsdir2lem4  27312  lgsdir2lem5  27313  gausslemma2dlem0i  27348  2lgslem3  27388  2lgslem4  27390  nosgnn0  27643  structiedg0val  29113  usgrexmplef  29350  3vfriswmgrlem  30370  prodpr  32924  cycpm2tr  33219  drngmxidlr  33577  lmat22lem  34001  signslema  34746  circlemethhgt  34827  subfacp1lem1  35401  subfacp1lem4  35405  rankeq1o  36393  onsucconni  36659  topdifinfindis  37628  poimirlem9  37909  divrngidl  38308  isfldidl  38348  dihmeetlem2N  41704  wopprc  43416  pw2f1ocnv  43423  kelac2lem  43450  prclaxpr  45370  permaxpr  45395  rnmptpr  45565  cncfiooicclem1  46280  paireqne  47900  31prm  47986  lighneallem4  47999  upgrimpths  48298  usgrexmpl2nb1  48421  usgrexmpl2nb2  48422  usgrexmpl2nb4  48424  usgrexmpl2nb5  48425  usgrexmpl2trifr  48426  pgnbgreunbgrlem3  48507  pgnbgreunbgrlem6  48513  nn0sumshdiglem2  49011  2arwcatlem1  49983  2arwcatlem5  49987  2arwcat  49988  onsetreclem3  50095