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

Theorem elpr2g 4552
 Description: A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) Generalize from sethood hypothesis to sethood antecedent. (Revised by BJ, 25-May-2024.)
Assertion
Ref Expression
elpr2g ((𝐵𝑉𝐶𝑊) → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))

Proof of Theorem elpr2g
StepHypRef Expression
1 elex 3462 . . 3 (𝐴 ∈ {𝐵, 𝐶} → 𝐴 ∈ V)
21a1i 11 . 2 ((𝐵𝑉𝐶𝑊) → (𝐴 ∈ {𝐵, 𝐶} → 𝐴 ∈ V))
3 elex 3462 . . . 4 (𝐵𝑉𝐵 ∈ V)
4 eleq1a 2888 . . . 4 (𝐵 ∈ V → (𝐴 = 𝐵𝐴 ∈ V))
53, 4syl 17 . . 3 (𝐵𝑉 → (𝐴 = 𝐵𝐴 ∈ V))
6 elex 3462 . . . 4 (𝐶𝑊𝐶 ∈ V)
7 eleq1a 2888 . . . 4 (𝐶 ∈ V → (𝐴 = 𝐶𝐴 ∈ V))
86, 7syl 17 . . 3 (𝐶𝑊 → (𝐴 = 𝐶𝐴 ∈ V))
95, 8jaao 952 . 2 ((𝐵𝑉𝐶𝑊) → ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐴 ∈ V))
10 elprg 4549 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
1110a1i 11 . 2 ((𝐵𝑉𝐶𝑊) → (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))))
122, 9, 11pm5.21ndd 384 1 ((𝐵𝑉𝐶𝑊) → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2112  Vcvv 3444  {cpr 4530 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531 This theorem is referenced by:  elpr2  4553
 Copyright terms: Public domain W3C validator