Theorem elpr 4609

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  difprsnss  4762  preq12b  4810  pwpr  4861  pwtp  4862  uniprg  4883  intprg  4941  axprALT  5384  zfpair2  5392  prex  5396  opthwiener  5487  tpres  7207  fnprb  7214  2oconcl  8511  pw2f1olem  9100  djuunxp  10002  sdom2en01  10380  gruun  10891  fzpr  13713  m1expeven  14252  bpoly2  16223  bpoly3  16224  lcmfpr  16802  isprm2  16857  gsumpr  20169  drngnidl  21531  psgninv  21888  psgnodpm  21894  mdetunilem7  22933  indistopon  23319  dfconn2  23737  cnconn  23740  unconn  23747  txindis  23953  txconn  24008  filconn  24202  xpsdsval  24700  rolle  26310  dvivthlem1  26328  ang180lem3  27139  ang180lem4  27140  wilthlem2  27396  sqff1o  27509  ppiub  27531  lgslem1  27624  lgsdir2lem4  27655  lgsdir2lem5  27656  gausslemma2dlem0i  27691  2lgslem3  27731  2lgslem4  27733  nosgnn0  28015  structiedg0val  29600  usgrexmplef  29840  3vfriswmgrlem  30878  prodpr  33417  cycpm2tr  33680  drngmxidlr  34002  lmat22lem  34449  signslema  35191  circlemethhgt  35272  subfacp1lem1  35944  subfacp1lem4  35948  rankeq1o  36932  onsucconni  37225  topdifinfindis  38269  poimirlem9  38547  impprop  38644  divrngidl  38962  isfldidl  39002  dihmeetlem2N  42356  wopprc  44036  pw2f1ocnv  44043  kelac2lem  44065  prclaxpr  45974  permaxpr  45999  rnmptpr  46191  cncfiooicclem1  46902  paireqne  48592  31prm  48681  lighneallem4  48694  upgrimpths  49006  usgrexmpl2nb1  49129  usgrexmpl2nb2  49130  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  usgrexmpl2trifr  49134  pgnbgreunbgrlem3  49215  pgnbgreunbgrlem6  49221  nn0sumshdiglem2  49733  2arwcatlem1  50702  2arwcatlem5  50706  2arwcat  50707  onsetreclem3  50799