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

Theorem elprg 3774
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 2393 . . 3  |-  ( x  =  A  ->  (
x  =  B  <->  A  =  B ) )
2 eqeq1 2393 . . 3  |-  ( x  =  A  ->  (
x  =  C  <->  A  =  C ) )
31, 2orbi12d 691 . 2  |-  ( x  =  A  ->  (
( x  =  B  \/  x  =  C )  <->  ( A  =  B  \/  A  =  C ) ) )
4 dfpr2 3773 . 2  |-  { B ,  C }  =  {
x  |  ( x  =  B  \/  x  =  C ) }
53, 4elab2g 3027 1  |-  ( A  e.  V  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    = wceq 1649    e. wcel 1717   {cpr 3758
This theorem is referenced by:  elpr  3775  elpr2  3776  elpri  3777  eltpg  3794  ifpr  3799  prid1g  3853  ordunpr  4746  hashtpg  11618  cnsubrg  16682  atandm  20583  nbgra0nb  21307  eupath2lem1  21547  eliccioo  24016  eldifpr  24188
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-un 3268  df-sn 3763  df-pr 3764
  Copyright terms: Public domain W3C validator