MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elprg Structured version   Visualization version   GIF version

Theorem elprg 4578
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.)
Assertion
Ref Expression
elprg (𝐴𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))

Proof of Theorem elprg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2822 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 eqeq1 2822 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐶𝐴 = 𝐶))
31, 2orbi12d 912 . 2 (𝑥 = 𝐴 → ((𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
4 dfpr2 4576 . 2 {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶)}
53, 4elab2g 3665 1 (𝐴𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wo 841   = wceq 1528  wcel 2105  {cpr 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-sn 4558  df-pr 4560
This theorem is referenced by:  elpri  4579  elpr  4580  elpr2  4581  nelpr2  4582  nelpr1  4583  eldifpr  4587  eltpg  4615  ifpr  4621  prid1g  4688  ssprss  4749  preq1b  4769  prel12g  4786  ordunpr  7530  hashtpg  13831  2nsgsimpgd  19153  cnsubrg  20533  atandm  25381  1egrvtxdg0  27220  eupth2lem1  27924  nelpr  30218  eliccioo  30534  linds2eq  30868  sfprmdvdsmersenne  43645  prelrrx2b  44629
  Copyright terms: Public domain W3C validator