Theorem elpr 4420

Description: A member of an unordered pair of classes is one or the other of them. 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 4418	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))

Syntax hints:   ↔ wb 198   ∨ wo 880   = wceq 1658   ∈ wcel 2166  Vcvv 3414  {cpr 4399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-sn 4398  df-pr 4400

This theorem is referenced by:  difprsnss  4548  preq12b  4597  prel12OLD  4598  pwpr  4652  pwtp  4653  unipr  4671  intpr  4730  axpr  5126  zfpair2  5128  opthwiener  5200  tpres  6722  fnprb  6728  2oconcl  7850  pw2f1olem  8333  djuunxp  9060  sdom2en01  9439  gruun  9943  fzpr  12689  m1expeven  13201  bpoly2  15160  bpoly3  15161  lcmfpr  15713  isprm2  15767  drngnidl  19590  psgninv  20287  psgnodpm  20293  mdetunilem7  20792  indistopon  21176  dfconn2  21593  cnconn  21596  unconn  21603  txindis  21808  txconn  21863  filconn  22057  xpsdsval  22556  rolle  24152  dvivthlem1  24170  ang180lem3  24951  ang180lem4  24952  wilthlem2  25208  sqff1o  25321  ppiub  25342  lgslem1  25435  lgsdir2lem4  25466  lgsdir2lem5  25467  gausslemma2dlem0i  25502  2lgslem3  25542  2lgslem4  25544  structiedg0val  26320  usgrexmplef  26556  3vfriswmgrlem  27658  prodpr  30119  lmat22lem  30428  signslema  31186  circlemethhgt  31270  subfacp1lem1  31707  subfacp1lem4  31711  nosgnn0  32350  rankeq1o  32817  onsucconni  32969  topdifinfindis  33739  poimirlem9  33962  divrngidl  34369  isfldidl  34409  dihmeetlem2N  37374  wopprc  38440  pw2f1ocnv  38447  kelac2lem  38477  rnmptpr  40167  cncfiooicclem1  40901  31prm  42342  lighneallem4  42357  gsumpr  42986  nn0sumshdiglem2  43263  onsetreclem3  43348