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

Theorem elprg 4647
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, 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 2740 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 eqeq1 2740 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐶𝐴 = 𝐶))
31, 2orbi12d 918 . 2 (𝑥 = 𝐴 → ((𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
4 dfpr2 4645 . 2 {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶)}
53, 4elab2g 3679 1 (𝐴𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wo 847   = wceq 1539  wcel 2107  {cpr 4627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-sn 4626  df-pr 4628
This theorem is referenced by:  elpri  4648  elpr  4649  elpr2g  4650  nelpr2  4652  nelpr1  4653  eldifpr  4657  eltpg  4685  ifpr  4692  prid1g  4759  ssprss  4823  preq1b  4845  prel12g  4863  ordunpr  7847  hashtpg  14525  2nsgsimpgd  20123  cnsubrg  21446  atandm  26920  1egrvtxdg0  29530  eupth2lem1  30238  nelpr  32550  eliccioo  32914  linds2eq  33410  sfprmdvdsmersenne  47595  prelrrx2b  48640
  Copyright terms: Public domain W3C validator