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

Theorem eldif 3316
Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldif  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )

Proof of Theorem eldif
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elex 2970 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2970 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 453 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2502 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2502 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 287 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 693 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3309 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 3090 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 344 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1727   _Vcvv 2962    \ cdif 3303
This theorem is referenced by:  eldifd  3317  eldifad  3318  eldifbd  3319  difeqri  3453  eldifi  3455  eldifn  3456  neldif  3458  difdif  3459  ddif  3465  ssconb  3466  sscon  3467  ssdif  3468  raldifb  3473  dfss4  3560  dfun2  3561  dfin2  3562  difin  3563  indifdir  3582  undif3  3587  difin2  3588  symdif2  3592  dfnul2  3615  reldisj  3695  disj3  3696  undif4  3708  ssdif0  3710  pssnel  3717  difin0ss  3718  inssdif0  3719  inundif  3730  ssundif  3735  eldifsn  3951  difprsnss  3958  iundif2  4182  iindif2  4184  disjss3  4236  brdif  4285  ordunidif  4658  onmindif  4700  eldifpw  4784  elpwunsn  4786  difopab  5035  intirr  5281  cnvdif  5307  imadif  5557  dffv2  5825  suppss  5892  suppssr  5893  suppss2  6329  difxp  6409  ondif2  6775  oelim2  6867  boxcutc  7134  brsdom  7159  brsdom2  7260  php3  7322  unblem1  7388  unfilem1  7400  elfi2  7448  dfsup2  7476  dfsup2OLD  7477  ordtypelem7  7522  cantnfreslem  7660  kmlem4  8064  ackbij1lem18  8148  infpssr  8219  isf34lem4  8288  fin17  8305  fin67  8306  dffin7-2  8309  fin1a2lem6  8316  axcclem  8368  pwfseqlem3  8566  grothprim  8740  xrlenlt  9174  irradd  10629  irrmul  10630  difreicc  11059  modirr  11317  hashinf  11654  sumss  12549  fsumss  12550  rpnnen2  12856  bitscmp  12981  iserodd  13240  sylow2alem2  15283  efgsfo  15402  gsumval3  15545  gsum2d  15577  ablfac1eu  15662  gsumdixp  15746  isnirred  15836  isirred2  15837  irredn0  15839  lsppratlem1  16250  lbsextlem2  16262  mplsubrglem  16533  mplcoe1  16559  mplcoe2  16561  opsrtoslem2  16576  elcls  17168  isclo  17182  maxlp  17242  restntr  17277  isreg2  17472  cmpcld  17496  hausdiag  17708  txkgen  17715  kqcldsat  17796  ufinffr  17992  fin1aufil  17995  alexsublem  18106  alexsubALTlem3  18111  ptcmplem5  18118  blcld  18566  shftmbl  19464  vitalilem4  19534  vitalilem5  19535  vitali  19536  mbfeqalem  19563  itg1val2  19605  itg10a  19631  itg1ge0a  19632  mbfi1fseqlem4  19639  itg2uba  19664  itg2splitlem  19669  itg2monolem1  19671  itg2cnlem1  19682  itg2cnlem2  19683  itgss  19732  dvtaylp  20317  pserdvlem2  20375  ellogdm  20561  atandm  20747  atans2  20802  wilthlem2  20883  basellem3  20896  fsumvma  21028  dchrelbas2  21052  dchreq  21073  dchrsum  21084  dchrisum0fno1  21236  rplogsum  21252  isusgra0  21407  nbcusgra  21503  eleigvec  23491  strlem1  23784  strlem5  23789  hstrlem5  23797  suppss2f  24080  xrdifh  24174  eldifpr  24423  eldiftp  24424  esumpinfval  24494  sibfof  24685  ballotlemodife  24786  ballotth  24826  eldmgm  24837  igamgam  24864  igamf  24866  igamcl  24867  lgam1  24879  gam1  24880  prodss  25304  fprodss  25305  dftr6  25404  dffr5  25407  wfi  25513  frind  25549  elsymdif  25699  brsset  25765  dfon3  25768  ellimits  25786  dffun10  25790  elfuns  25791  fullfunfv  25823  dfrdg4  25826  tfrqfree  25827  dfint3  25828  hfext  26155  onsucsuccmpi  26224  iundif1  26268  dvtanlem  26292  itg2addnclem  26294  ftc1anclem5  26322  areacirc  26335  fdc  26487  isfldidl  26716  ellz1  26863  pellexlem4  26933  pellexlem5  26934  compel  27655  stoweidlem26  27789  stoweidlem39  27802  stoweidlem52  27815  uhgraedgrnv  28350  frgraunss  28483  frgrancvvdeqlem3  28519  frgrancvvdeqlem9  28528  frgrawopreglem3  28533  frgrawopreglem4  28534  frgrawopreg  28536  usg2spot2nb  28552  undif3VD  29092  iswatN  30889  dochsnkrlem1  32365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-dif 3309
  Copyright terms: Public domain W3C validator