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

Theorem eldif 3322
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 2956 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2956 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 452 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2495 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2495 . . . . 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 3315 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 3076 . 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 1652    e. wcel 1725   _Vcvv 2948    \ cdif 3309
This theorem is referenced by:  eldifd  3323  eldifad  3324  eldifbd  3325  difeqri  3459  eldifi  3461  eldifn  3462  neldif  3464  difdif  3465  ddif  3471  ssconb  3472  sscon  3473  ssdif  3474  raldifb  3479  dfss4  3567  dfun2  3568  dfin2  3569  difin  3570  indifdir  3589  undif3  3594  difin2  3595  symdif2  3599  dfnul2  3622  reldisj  3663  disj3  3664  undif4  3676  ssdif0  3678  pssnel  3685  difin0ss  3686  inssdif0  3687  inundif  3698  ssundif  3703  eldifsn  3919  difprsnss  3926  iundif2  4150  iindif2  4152  disjss3  4203  brdif  4252  ordunidif  4621  onmindif  4663  eldifpw  4747  elpwunsn  4749  difopab  4998  intirr  5244  cnvdif  5270  imadif  5520  dffv2  5788  suppss  5855  suppssr  5856  suppss2  6292  difxp  6372  ondif2  6738  oelim2  6830  boxcutc  7097  brsdom  7122  brsdom2  7223  php3  7285  unblem1  7351  unfilem1  7363  elfi2  7411  dfsup2  7439  dfsup2OLD  7440  ordtypelem7  7485  cantnfreslem  7623  kmlem4  8025  ackbij1lem18  8109  infpssr  8180  isf34lem4  8249  fin17  8266  fin67  8267  dffin7-2  8270  fin1a2lem6  8277  axcclem  8329  pwfseqlem3  8527  grothprim  8701  xrlenlt  9135  irradd  10590  irrmul  10591  difreicc  11020  modirr  11278  hashinf  11615  sumss  12510  fsumss  12511  rpnnen2  12817  bitscmp  12942  iserodd  13201  sylow2alem2  15244  efgsfo  15363  gsumval3  15506  gsum2d  15538  ablfac1eu  15623  gsumdixp  15707  isnirred  15797  isirred2  15798  irredn0  15800  lsppratlem1  16211  lbsextlem2  16223  mplsubrglem  16494  mplcoe1  16520  mplcoe2  16522  opsrtoslem2  16537  elcls  17129  isclo  17143  maxlp  17203  restntr  17238  isreg2  17433  cmpcld  17457  hausdiag  17669  txkgen  17676  kqcldsat  17757  ufinffr  17953  fin1aufil  17956  alexsublem  18067  alexsubALTlem3  18072  ptcmplem5  18079  blcld  18527  shftmbl  19425  vitalilem4  19495  vitalilem5  19496  vitali  19497  mbfeqalem  19526  itg1val2  19568  itg10a  19594  itg1ge0a  19595  mbfi1fseqlem4  19602  itg2uba  19627  itg2splitlem  19632  itg2monolem1  19634  itg2cnlem1  19645  itg2cnlem2  19646  itgss  19695  dvtaylp  20278  pserdvlem2  20336  ellogdm  20522  atandm  20708  atans2  20763  wilthlem2  20844  basellem3  20857  fsumvma  20989  dchrelbas2  21013  dchreq  21034  dchrsum  21045  dchrisum0fno1  21197  rplogsum  21213  isusgra0  21368  nbcusgra  21464  eleigvec  23452  strlem1  23745  strlem5  23750  hstrlem5  23758  suppss2f  24041  xrdifh  24135  eldifpr  24384  eldiftp  24385  esumpinfval  24455  sibfof  24646  ballotlemodife  24747  ballotth  24787  eldmgm  24798  igamgam  24825  igamf  24827  igamcl  24828  lgam1  24840  gam1  24841  prodss  25265  fprodss  25266  dftr6  25365  dffr5  25368  wfi  25474  frind  25510  elsymdif  25660  brsset  25726  dfon3  25729  ellimits  25747  dffun10  25751  elfuns  25752  fullfunfv  25784  dfrdg4  25787  tfrqfree  25788  dfint3  25789  hfext  26116  onsucsuccmpi  26185  itg2addnclem  26246  areacirc  26278  fdc  26430  isfldidl  26659  ellz1  26806  pellexlem4  26876  pellexlem5  26877  compel  27598  stoweidlem26  27732  stoweidlem39  27745  stoweidlem52  27758  uhgraedgrnv  28245  frgraunss  28312  frgrancvvdeqlem3  28348  frgrancvvdeqlem9  28357  frgrawopreglem3  28362  frgrawopreglem4  28363  frgrawopreg  28365  usg2spot2nb  28381  undif3VD  28921  iswatN  30718  dochsnkrlem1  32194
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315
  Copyright terms: Public domain W3C validator