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

Theorem elpr2 4337
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) (Proof shortened by JJ, 23-Jul-2021.)
Hypotheses
Ref Expression
elpr2.1 𝐵 ∈ V
elpr2.2 𝐶 ∈ V
Assertion
Ref Expression
elpr2 (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))

Proof of Theorem elpr2
StepHypRef Expression
1 elex 3361 . 2 (𝐴 ∈ {𝐵, 𝐶} → 𝐴 ∈ V)
2 elpr2.1 . . . 4 𝐵 ∈ V
3 eleq1 2837 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
42, 3mpbiri 248 . . 3 (𝐴 = 𝐵𝐴 ∈ V)
5 elpr2.2 . . . 4 𝐶 ∈ V
6 eleq1 2837 . . . 4 (𝐴 = 𝐶 → (𝐴 ∈ V ↔ 𝐶 ∈ V))
75, 6mpbiri 248 . . 3 (𝐴 = 𝐶𝐴 ∈ V)
84, 7jaoi 837 . 2 ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐴 ∈ V)
9 elprg 4334 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
101, 8, 9pm5.21nii 367 1 (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 826   = wceq 1630  wcel 2144  Vcvv 3349  {cpr 4316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726  df-sn 4315  df-pr 4317
This theorem is referenced by:  elopg  5062  elxr  12154  fprodex01  29905  nofv  32141
  Copyright terms: Public domain W3C validator