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

Theorem elprg 4653
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 2739 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 eqeq1 2739 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐶𝐴 = 𝐶))
31, 2orbi12d 918 . 2 (𝑥 = 𝐴 → ((𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
4 dfpr2 4651 . 2 {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶)}
53, 4elab2g 3683 1 (𝐴𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wo 847   = wceq 1537  wcel 2106  {cpr 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634
This theorem is referenced by:  elpri  4654  elpr  4655  elpr2g  4656  nelpr2  4658  nelpr1  4659  eldifpr  4663  eltpg  4691  ifpr  4698  prid1g  4765  ssprss  4829  preq1b  4851  prel12g  4869  ordunpr  7846  hashtpg  14521  2nsgsimpgd  20137  cnsubrg  21463  atandm  26934  1egrvtxdg0  29544  eupth2lem1  30247  nelpr  32557  eliccioo  32898  linds2eq  33389  sfprmdvdsmersenne  47528  prelrrx2b  48564
  Copyright terms: Public domain W3C validator