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

Theorem eldif 3275
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 2909 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2909 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 452 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2449 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2449 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 286 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 692 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3268 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 3029 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 343 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2901    \ cdif 3262
This theorem is referenced by:  eldifd  3276  eldifad  3277  eldifbd  3278  difeqri  3412  eldifi  3414  eldifn  3415  neldif  3417  difdif  3418  ddif  3424  ssconb  3425  sscon  3426  ssdif  3427  raldifb  3432  dfss4  3520  dfun2  3521  dfin2  3522  difin  3523  indifdir  3542  undif3  3547  difin2  3548  symdif2  3552  dfnul2  3575  reldisj  3616  disj3  3617  undif4  3629  ssdif0  3631  pssnel  3638  difin0ss  3639  inssdif0  3640  inundif  3651  ssundif  3656  eldifsn  3872  difprsnss  3879  iundif2  4101  iindif2  4103  disjss3  4154  brdif  4203  ordunidif  4572  onmindif  4613  eldifpw  4697  elpwunsn  4699  difopab  4948  intirr  5194  cnvdif  5220  imadif  5470  dffv2  5737  suppss  5804  suppssr  5805  suppss2  6241  difxp  6321  ondif2  6684  oelim2  6776  boxcutc  7043  brsdom  7068  brsdom2  7169  php3  7231  unblem1  7297  unfilem1  7309  elfi2  7356  dfsup2  7384  dfsup2OLD  7385  ordtypelem7  7428  cantnfreslem  7566  kmlem4  7968  ackbij1lem18  8052  infpssr  8123  isf34lem4  8192  fin17  8209  fin67  8210  dffin7-2  8213  fin1a2lem6  8220  axcclem  8272  pwfseqlem3  8470  grothprim  8644  xrlenlt  9078  irradd  10532  irrmul  10533  difreicc  10962  modirr  11215  hashinf  11552  sumss  12447  fsumss  12448  rpnnen2  12754  bitscmp  12879  iserodd  13138  sylow2alem2  15181  efgsfo  15300  gsumval3  15443  gsum2d  15475  ablfac1eu  15560  gsumdixp  15644  isnirred  15734  isirred2  15735  irredn0  15737  lsppratlem1  16148  lbsextlem2  16160  mplsubrglem  16431  mplcoe1  16457  mplcoe2  16459  opsrtoslem2  16474  elcls  17062  isclo  17076  maxlp  17135  restntr  17170  isreg2  17365  cmpcld  17389  hausdiag  17600  txkgen  17607  kqcldsat  17688  ufinffr  17884  fin1aufil  17887  alexsublem  17998  alexsubALTlem3  18003  ptcmplem5  18010  blcld  18427  shftmbl  19302  vitalilem4  19372  vitalilem5  19373  vitali  19374  mbfeqalem  19403  itg1val2  19445  itg10a  19471  itg1ge0a  19472  mbfi1fseqlem4  19479  itg2uba  19504  itg2splitlem  19509  itg2monolem1  19511  itg2cnlem1  19522  itg2cnlem2  19523  itgss  19572  dvtaylp  20155  pserdvlem2  20213  ellogdm  20399  atandm  20585  atans2  20640  wilthlem2  20721  basellem3  20734  fsumvma  20866  dchrelbas2  20890  dchreq  20911  dchrsum  20922  dchrisum0fno1  21074  rplogsum  21090  isusgra0  21245  nbcusgra  21340  eleigvec  23310  strlem1  23603  strlem5  23608  hstrlem5  23616  suppss2f  23894  xrdifh  23981  eldifpr  24190  eldiftp  24191  esumpinfval  24261  ballotlemodife  24536  ballotth  24576  eldmgm  24587  igamgam  24614  igamf  24616  igamcl  24617  lgam1  24629  gam1  24630  prodss  25054  fprodss  25055  dftr6  25133  dffr5  25136  wfi  25233  frind  25269  elsymdif  25393  brsset  25455  dfon3  25458  ellimits  25476  elfuns  25480  fullfunfv  25512  dfrdg4  25515  tfrqfree  25516  hfext  25840  onsucsuccmpi  25909  itg2addnclem  25959  areacirc  25990  fdc  26142  isfldidl  26371  ellz1  26518  pellexlem4  26588  pellexlem5  26589  compel  27311  stoweidlem26  27445  stoweidlem39  27458  stoweidlem52  27471  frgraunss  27750  frgrancvvdeqlem3  27786  frgrancvvdeqlem9  27795  frgrawopreglem3  27800  frgrawopreglem4  27801  frgrawopreg  27803  undif3VD  28337  iswatN  30110  dochsnkrlem1  31586
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 2370
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 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-dif 3268
  Copyright terms: Public domain W3C validator