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

Theorem elprg 3983
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.)
Assertion
Ref Expression
elprg  |-  ( A  e.  V  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )

Proof of Theorem elprg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2454 . . 3  |-  ( x  =  A  ->  (
x  =  B  <->  A  =  B ) )
2 eqeq1 2454 . . 3  |-  ( x  =  A  ->  (
x  =  C  <->  A  =  C ) )
31, 2orbi12d 715 . 2  |-  ( x  =  A  ->  (
( x  =  B  \/  x  =  C )  <->  ( A  =  B  \/  A  =  C ) ) )
4 dfpr2 3982 . 2  |-  { B ,  C }  =  {
x  |  ( x  =  B  \/  x  =  C ) }
53, 4elab2g 3186 1  |-  ( A  e.  V  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    \/ wo 370    = wceq 1443    e. wcel 1886   {cpr 3969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-un 3408  df-sn 3968  df-pr 3970
This theorem is referenced by:  elpri  3984  elpr  3985  elpr2  3986  eldifpr  3989  eltpg  4013  ifpr  4019  prid1g  4077  preq1b  4145  ordunpr  6650  hashtpg  12638  cnsubrg  19021  atandm  23795  nbgra0nb  25150  eupath2lem1  25698  eliccioo  28393  ssprss  38995
  Copyright terms: Public domain W3C validator