ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elpri Unicode version

Theorem elpri 3518
Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.)
Assertion
Ref Expression
elpri  |-  ( A  e.  { B ,  C }  ->  ( A  =  B  \/  A  =  C ) )

Proof of Theorem elpri
StepHypRef Expression
1 elprg 3515 . 2  |-  ( A  e.  { B ,  C }  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
21ibi 175 1  |-  ( A  e.  { B ,  C }  ->  ( A  =  B  \/  A  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 680    = wceq 1314    e. wcel 1463   {cpr 3496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502
This theorem is referenced by:  nelpri  3519  nelprd  3521  opth1  4126  0nelop  4138  ontr2exmid  4408  onintexmid  4455  reg3exmidlemwe  4461  funtpg  5142  ftpg  5570  acexmidlemcase  5735  2oconcl  6302  en2eqpr  6767  eldju1st  6922  finomni  6978  exmidomniim  6979  ismkvnex  6995  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidaclem  7028  sup3exmid  8675  m1expcl2  10266  maxleim  10928  maxleast  10936  zmaxcl  10947  minmax  10952  xrmaxleim  10964  xrmaxaddlem  10980  xrminmax  10985  unct  11860  qtopbas  12597  limcimolemlt  12708  recnprss  12731  el2oss1o  13022  nninfalllem1  13037  nninfall  13038  nninfsellemqall  13045  nninfomnilem  13048  isomninnlem  13059  trilpolemclim  13063  trilpolemcl  13064  trilpolemisumle  13065  trilpolemeq1  13067  trilpolemlt1  13068
  Copyright terms: Public domain W3C validator