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

Theorem eldifpr 4033
Description: Membership in a set with two elements removed. Similar to eldifsn 4141 and eldiftp 4059. (Contributed by Mario Carneiro, 18-Jul-2017.)
Assertion
Ref Expression
eldifpr  |-  ( A  e.  ( B  \  { C ,  D }
)  <->  ( A  e.  B  /\  A  =/= 
C  /\  A  =/=  D ) )

Proof of Theorem eldifpr
StepHypRef Expression
1 elprg 4032 . . . . 5  |-  ( A  e.  B  ->  ( A  e.  { C ,  D }  <->  ( A  =  C  \/  A  =  D ) ) )
21notbid 292 . . . 4  |-  ( A  e.  B  ->  ( -.  A  e.  { C ,  D }  <->  -.  ( A  =  C  \/  A  =  D )
) )
3 neanior 2779 . . . 4  |-  ( ( A  =/=  C  /\  A  =/=  D )  <->  -.  ( A  =  C  \/  A  =  D )
)
42, 3syl6bbr 263 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C ,  D }  <->  ( A  =/=  C  /\  A  =/= 
D ) ) )
54pm5.32i 635 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C ,  D } )  <->  ( A  e.  B  /\  ( A  =/=  C  /\  A  =/=  D ) ) )
6 eldif 3471 . 2  |-  ( A  e.  ( B  \  { C ,  D }
)  <->  ( A  e.  B  /\  -.  A  e.  { C ,  D } ) )
7 3anass 975 . 2  |-  ( ( A  e.  B  /\  A  =/=  C  /\  A  =/=  D )  <->  ( A  e.  B  /\  ( A  =/=  C  /\  A  =/=  D ) ) )
85, 6, 73bitr4i 277 1  |-  ( A  e.  ( B  \  { C ,  D }
)  <->  ( A  e.  B  /\  A  =/= 
C  /\  A  =/=  D ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 366    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823    =/= wne 2649    \ cdif 3458   {cpr 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-un 3466  df-sn 4017  df-pr 4019
This theorem is referenced by:  logbcl  23306  logbid1  23307  logb1  23308  elogb  23309  logbchbase  23310  relogbval  23311  relogbcl  23312  relogbreexp  23314  relogbmul  23316  relogbexp  23319  nnlogbexp  23320  relogbcxp  23324  cxplogb  23325  relogbcxpb  23326  logbmpt  23327  logbfval  23329  rexdifpr  32674  eluz2cnn0n1  33369  rege1logbrege0  33433  relogbmulbexp  33436  relogbdivb  33437  nnpw2blen  33455
  Copyright terms: Public domain W3C validator