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

Theorem elprg 4605
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 2741 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 eqeq1 2741 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝐶𝐴 = 𝐶))
31, 2orbi12d 917 . 2 (𝑥 = 𝐴 → ((𝑥 = 𝐵𝑥 = 𝐶) ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
4 dfpr2 4603 . 2 {𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐵𝑥 = 𝐶)}
53, 4elab2g 3630 1 (𝐴𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wo 845   = wceq 1541  wcel 2106  {cpr 4586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-un 3913  df-sn 4585  df-pr 4587
This theorem is referenced by:  elpri  4606  elpr  4607  elpr2g  4608  elpr2OLD  4610  nelpr2  4611  nelpr1  4612  eldifpr  4616  eltpg  4644  ifpr  4650  prid1g  4719  ssprss  4782  preq1b  4802  prel12g  4819  ordunpr  7753  hashtpg  14338  2nsgsimpgd  19840  cnsubrg  20810  atandm  26178  1egrvtxdg0  28288  eupth2lem1  28991  nelpr  31287  eliccioo  31613  linds2eq  31994  sfprmdvdsmersenne  45696  prelrrx2b  46701
  Copyright terms: Public domain W3C validator