Theorem eldif 3333

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.

Step	Hyp	Ref	Expression
1		elex 2976	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2976	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 465	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2498	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2498	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 294	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 710	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3326	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3103	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 353	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   _Vcvv 2967   \ cdif 3320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-dif 3326

This theorem is referenced by:  eldifd  3334  eldifad  3335  eldifbd  3336  difeqri  3471  eldifi  3473  eldifn  3474  neldif  3476  difdif  3477  ddif  3483  ssconb  3484  sscon  3485  ssdif  3486  raldifb  3491  dfss4  3579  dfun2  3580  dfin2  3581  difin  3582  indifdir  3601  undif3  3606  difin2  3607  symdif2  3611  dfnul2  3634  reldisj  3717  disj3  3718  undif4  3730  ssdif0  3732  pssnel  3739  difin0ss  3740  inssdif0  3741  inundif  3752  ssundif  3757  eldifpr  3889  elpwunsn  3912  eldiftp  3914  eldifsn  3995  difprsnss  4004  iundif2  4232  iindif2  4234  disjss3  4286  brdif  4337  ordunidif  4762  onmindif  4803  difopab  4966  intirr  5211  cnvdif  5238  difxp  5257  xpdifid  5261  imadif  5488  dffv2  5759  suppssOLD  5831  suppssrOLD  5832  suppss2OLD  6310  eldifpw  6383  ressuppssdif  6705  extmptsuppeq  6708  suppss  6714  suppssr  6715  suppss2  6718  ondif2  6934  oelim2  7026  boxcutc  7298  brsdom  7324  brsdom2  7427  php3  7489  unblem1  7556  unfilem1  7568  elfi2  7656  dfsup2  7684  dfsup2OLD  7685  ordtypelem7  7730  kmlem4  8314  ackbij1lem18  8398  infpssr  8469  isf34lem4  8538  fin17  8555  fin67  8556  dffin7-2  8559  fin1a2lem6  8566  axcclem  8618  pwfseqlem3  8819  grothprim  8993  xrlenlt  9434  irradd  10969  irrmul  10970  difreicc  11409  modirr  11761  hashinf  12100  sumss  13193  fsumss  13194  rpnnen2  13500  bitscmp  13626  iserodd  13894  symgfix2  15912  pmtrdifellem4  15976  sylow2alem2  16108  efgsfo  16227  gsumval3OLD  16373  gsumval3  16376  gsum2dlem1  16451  gsum2dlem2  16452  gsum2dOLD  16454  ablfac1eu  16564  gsumdixpOLD  16690  gsumdixp  16691  isnirred  16782  isirred2  16783  irredn0  16785  lsppratlem1  17208  lbsextlem2  17220  mplsubrglem  17497  mplsubrglemOLD  17498  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  opsrtoslem2  17546  psgnodpm  17998  symgmatr01lem  18439  elcls  18657  isclo  18671  maxlp  18731  restntr  18766  isreg2  18961  cmpcld  18985  hausdiag  19198  txkgen  19205  kqcldsat  19286  ufinffr  19482  fin1aufil  19485  alexsublem  19596  alexsubALTlem3  19601  ptcmplem5  19608  blcld  20060  shftmbl  21000  vitalilem4  21071  vitalilem5  21072  vitali  21073  mbfeqalem  21100  itg1val2  21142  itg10a  21168  itg1ge0a  21169  mbfi1fseqlem4  21176  itg2uba  21201  itg2splitlem  21206  itg2monolem1  21208  itg2cnlem1  21219  itg2cnlem2  21220  itgss  21269  dvtaylp  21815  pserdvlem2  21873  ellogdm  22064  atandm  22251  atans2  22306  wilthlem2  22387  basellem3  22400  fsumvma  22532  dchrelbas2  22556  dchreq  22577  dchrsum  22588  dchrisum0fno1  22740  rplogsum  22756  isusgra0  23243  nbcusgra  23339  eleigvec  25329  strlem1  25622  strlem5  25627  hstrlem5  25635  suppss2f  25922  suppss3  25995  xrdifh  26038  nndiffz1  26043  ordtconlem1  26323  esumpinfval  26491  eulerpartlems  26712  eulerpartlemgc  26714  eulerpartlemb  26720  eulerpartlemf  26722  eulerpartlemt  26723  eulerpartlemgh  26730  ballotlemodife  26849  ballotth  26889  eldmgm  26977  igamgam  27004  igamf  27006  igamcl  27007  lgam1  27019  gam1  27020  prodss  27429  fprodss  27430  dftr6  27529  dffr5  27532  wfi  27637  frind  27673  elsymdif  27823  brsset  27889  dfon3  27892  ellimits  27910  dffun10  27914  elfuns  27915  fullfunfv  27947  dfrdg4  27950  tfrqfree  27951  dfint3  27952  hfext  28190  onsucsuccmpi  28259  iundif1  28384  dvtanlem  28412  itg2addnclem  28414  ftc1anclem5  28442  areacirc  28460  fdc  28612  isfldidl  28839  ellz1  29076  pellexlem4  29144  pellexlem5  29145  compel  29665  stoweidlem26  29792  stoweidlem39  29805  stoweidlem52  29818  uhgraedgrnv  30244  frgraunss  30558  frgrancvvdeqlem3  30596  frgrancvvdeqlem9  30605  frgrawopreglem3  30610  frgrawopreglem4  30611  frgrawopreg  30613  usg2spot2nb  30629  lindslinindsimp1  30922  undif3VD  31547  iswatN  33531  dochsnkrlem1  35007