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

Theorem eldif 3175
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 2809 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2809 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 451 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2356 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2356 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 285 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 691 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3168 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 2929 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 342 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   _Vcvv 2801    \ cdif 3162
This theorem is referenced by:  eldifd  3176  eldifad  3177  eldifbd  3178  difeqri  3309  eldifi  3311  eldifn  3312  neldif  3314  difdif  3315  ddif  3321  ssconb  3322  sscon  3323  ssdif  3324  dfss4  3416  dfun2  3417  dfin2  3418  difin  3419  indifdir  3438  undif3  3442  difin2  3443  symdif2  3447  dfnul2  3470  reldisj  3511  disj3  3512  undif4  3524  ssdif0  3526  pssnel  3532  difin0ss  3533  inssdif0  3534  inundif  3545  ssundif  3550  eldifsn  3762  difprsnss  3769  iundif2  3985  iindif2  3987  disjss3  4038  brdif  4087  pwundifOLD  4317  ordunidif  4456  onmindif  4498  eldifpw  4582  elpwunsn  4584  difopab  4833  intirr  5077  cnvdif  5103  imadif  5343  dffv2  5608  suppss  5674  suppssr  5675  suppss2  6089  difxp  6169  ondif2  6517  oaf1o  6577  oelim2  6609  boxcutc  6875  brsdom  6900  brsdom2  7001  php3  7063  unblem1  7125  unfilem1  7137  elfi2  7184  dfsup2  7211  dfsup2OLD  7212  ordtypelem7  7255  infeq5i  7353  cantnfreslem  7393  cantnflem1  7407  cantnflem2  7408  kmlem4  7795  ackbij1lem18  7879  infpssr  7950  fin23lem26  7967  isf34lem4  8019  fin17  8036  fin67  8037  isfin7-2  8038  dffin7-2  8040  fin1a2lem6  8047  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  ttukeylem7  8158  pwfseqlem1  8296  pwfseqlem3  8298  grothprim  8472  xrlenlt  8906  irradd  10356  irrmul  10357  difreicc  10783  modirr  11025  hashinf  11358  hashf1lem1  11409  seqcoll  11417  seqcoll2  11418  rlimcld2  12068  sumrblem  12200  fsumcvg  12201  sumss  12213  fsumss  12214  rpnnen2  12520  ruclem12  12535  bitscmp  12645  iserodd  12904  prmreclem5  12983  ramub1lem1  13089  sylow2alem2  14945  efgsfo  15064  frgpnabllem1  15177  gsumval3  15207  gsumzaddlem  15219  gsum2d  15239  dmdprdsplitlem  15288  ablfac1eu  15324  pgpfac1lem2  15326  pgpfac1lem3  15328  gsumdixp  15408  isnirred  15498  isirred2  15499  irredn0  15501  irredrmul  15505  lsppratlem1  15916  lsppratlem3  15918  lbsextlem2  15928  lbsextlem4  15930  mplsubrglem  16199  mplcoe1  16225  mplcoe2  16227  opsrtoslem2  16242  elcls  16826  isclo  16840  maxlp  16894  restntr  16928  regsep2  17120  isreg2  17121  cmpcld  17145  1stckgen  17265  hausdiag  17355  txkgen  17362  kqcldsat  17440  regr1lem  17446  ufinffr  17640  fin1aufil  17643  alexsublem  17754  alexsubALTlem3  17759  ptcmplem5  17766  opnsubg  17806  blcld  18067  zcld  18335  recld2  18336  bcthlem4  18765  shftmbl  18912  iundisj  18921  vitalilem4  18982  vitalilem5  18983  vitali  18984  mbfeqalem  19013  itg1val2  19055  itg10a  19081  itg1ge0a  19082  mbfi1fseqlem4  19089  itg2uba  19114  itg2splitlem  19119  itg2monolem1  19121  itg2cnlem1  19132  itg2cnlem2  19133  iblss2  19176  itgss  19182  itgeqa  19184  limcnlp  19244  dvtaylp  19765  pserdvlem2  19820  ellogdm  20002  dvloglem  20011  dvlog2lem  20015  atandm  20188  atans2  20243  ressatans  20246  wilthlem2  20323  ftalem3  20328  basellem3  20336  fsumvma  20468  dchrelbas2  20492  dchreq  20513  dchrsum  20524  dchrisum0fno1  20676  rplogsum  20692  eleigvec  22553  strlem1  22846  strlem5  22851  hstrlem5  22859  ballotlemodife  23072  suppss2f  23216  xrdifh  23288  iundisjfi  23378  iundisjf  23380  eldifpr  23409  eldiftp  23410  esumpinfval  23456  eldmgm  23709  dftr6  24178  dffr5  24181  wfi  24278  frind  24314  elsymdif  24438  brsset  24500  dfon3  24503  ellimits  24521  elfuns  24525  fullfunfv  24557  dfrdg4  24560  tfrqfree  24561  hfext  24885  onsucsuccmpi  24954  onint1  24960  itg2addnclem  25003  areacirc  25034  difeqri2  25143  deref  25391  gltpntl2  26176  lppotos  26247  pdiveql  26271  abhp  26276  fdc  26558  isfldidl  26796  pridlc3  26801  prtlem80  26827  ellz1  26949  pellexlem4  27020  pellexlem5  27021  rmspecsqrnq  27094  rmspecnonsq  27095  frlmsslsp  27351  compel  27743  stoweidlem26  27878  stoweidlem34  27886  stoweidlem39  27891  stoweidlem52  27904  stoweidlem57  27909  stirlinglem8  27933  isusgra0  28238  nbcusgra  28298  undif3VD  28974  iswatN  30805  dochsnkrlem1  32281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168
  Copyright terms: Public domain W3C validator