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

Theorem elprg 4143
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 2613 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 eqeq1 2613 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐶𝐴 = 𝐶))
31, 2orbi12d 741 . 2 (𝑥 = 𝐴 → ((𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
4 dfpr2 4142 . 2 {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶)}
53, 4elab2g 3321 1 (𝐴𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381   = wceq 1474  wcel 1976  {cpr 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-sn 4125  df-pr 4127
This theorem is referenced by:  elpri  4144  elpr  4145  elpr2  4146  elpr2OLD  4147  eldifpr  4151  eltpg  4173  ifpr  4179  prid1g  4238  preq1b  4312  ordunpr  6895  hashtpg  13071  cnsubrg  19571  atandm  24320  nbgra0nb  25724  eupath2lem1  26270  eliccioo  28776  nelpr2  38084  nelpr1  38085  sfprmdvdsmersenne  39856  ssprss  40121  1egrvtxdg0  40722  eupth2lem1  41381
  Copyright terms: Public domain W3C validator