Theorem eldif 3326

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 2971	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2971	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 462	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2493	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2493	. . . . 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 703	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3319	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3097	. 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 1362   e. wcel 1755   _Vcvv 2962   \ cdif 3313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319

This theorem is referenced by:  eldifd  3327  eldifad  3328  eldifbd  3329  difeqri  3464  eldifi  3466  eldifn  3467  neldif  3469  difdif  3470  ddif  3476  ssconb  3477  sscon  3478  ssdif  3479  raldifb  3484  dfss4  3572  dfun2  3573  dfin2  3574  difin  3575  indifdir  3594  undif3  3599  difin2  3600  symdif2  3604  dfnul2  3627  reldisj  3710  disj3  3711  undif4  3723  ssdif0  3725  pssnel  3732  difin0ss  3733  inssdif0  3734  inundif  3745  ssundif  3750  eldifpr  3882  elpwunsn  3905  eldiftp  3907  eldifsn  3988  difprsnss  3997  iundif2  4225  iindif2  4227  disjss3  4279  brdif  4330  ordunidif  4754  onmindif  4795  difopab  4958  intirr  5204  cnvdif  5231  difxp  5250  xpdifid  5254  imadif  5481  dffv2  5752  suppssOLD  5824  suppssrOLD  5825  suppss2OLD  6304  eldifpw  6377  ressuppssdif  6699  extmptsuppeq  6702  suppss  6708  suppssr  6709  suppss2  6712  ondif2  6930  oelim2  7022  boxcutc  7294  brsdom  7320  brsdom2  7423  php3  7485  unblem1  7552  unfilem1  7564  elfi2  7652  dfsup2  7680  dfsup2OLD  7681  ordtypelem7  7726  kmlem4  8310  ackbij1lem18  8394  infpssr  8465  isf34lem4  8534  fin17  8551  fin67  8552  dffin7-2  8555  fin1a2lem6  8562  axcclem  8614  pwfseqlem3  8815  grothprim  8989  xrlenlt  9430  irradd  10965  irrmul  10966  difreicc  11404  modirr  11753  hashinf  12092  sumss  13185  fsumss  13186  rpnnen2  13491  bitscmp  13617  iserodd  13885  symgfix2  15901  pmtrdifellem4  15965  sylow2alem2  16097  efgsfo  16216  gsumval3OLD  16362  gsumval3  16365  gsum2dlem1  16435  gsum2dlem2  16436  gsum2dOLD  16438  ablfac1eu  16548  gsumdixpOLD  16635  gsumdixp  16636  isnirred  16726  isirred2  16727  irredn0  16729  lsppratlem1  17150  lbsextlem2  17162  mplsubrglem  17451  mplsubrglemOLD  17452  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  opsrtoslem2  17498  psgnodpm  17860  symgmatr01lem  18301  elcls  18519  isclo  18533  maxlp  18593  restntr  18628  isreg2  18823  cmpcld  18847  hausdiag  19060  txkgen  19067  kqcldsat  19148  ufinffr  19344  fin1aufil  19347  alexsublem  19458  alexsubALTlem3  19463  ptcmplem5  19470  blcld  19922  shftmbl  20862  vitalilem4  20933  vitalilem5  20934  vitali  20935  mbfeqalem  20962  itg1val2  21004  itg10a  21030  itg1ge0a  21031  mbfi1fseqlem4  21038  itg2uba  21063  itg2splitlem  21068  itg2monolem1  21070  itg2cnlem1  21081  itg2cnlem2  21082  itgss  21131  dvtaylp  21720  pserdvlem2  21778  ellogdm  21969  atandm  22156  atans2  22211  wilthlem2  22292  basellem3  22305  fsumvma  22437  dchrelbas2  22461  dchreq  22482  dchrsum  22493  dchrisum0fno1  22645  rplogsum  22661  isusgra0  23098  nbcusgra  23194  eleigvec  25184  strlem1  25477  strlem5  25482  hstrlem5  25490  suppss2f  25778  suppss3  25851  xrdifh  25893  nndiffz1  25898  ordtconlem1  26208  esumpinfval  26376  eulerpartlems  26591  eulerpartlemgc  26593  eulerpartlemb  26599  eulerpartlemf  26601  eulerpartlemt  26602  eulerpartlemgh  26609  ballotlemodife  26728  ballotth  26768  eldmgm  26856  igamgam  26883  igamf  26885  igamcl  26886  lgam1  26898  gam1  26899  prodss  27307  fprodss  27308  dftr6  27407  dffr5  27410  wfi  27515  frind  27551  elsymdif  27701  brsset  27767  dfon3  27770  ellimits  27788  dffun10  27792  elfuns  27793  fullfunfv  27825  dfrdg4  27828  tfrqfree  27829  dfint3  27830  hfext  28068  onsucsuccmpi  28137  iundif1  28257  dvtanlem  28285  itg2addnclem  28287  ftc1anclem5  28315  areacirc  28333  fdc  28485  isfldidl  28712  ellz1  28950  pellexlem4  29018  pellexlem5  29019  compel  29539  stoweidlem26  29667  stoweidlem39  29680  stoweidlem52  29693  uhgraedgrnv  30119  frgraunss  30433  frgrancvvdeqlem3  30471  frgrancvvdeqlem9  30480  frgrawopreglem3  30485  frgrawopreglem4  30486  frgrawopreg  30488  usg2spot2nb  30504  lindslinindsimp1  30700  undif3VD  31320  iswatN  33211  dochsnkrlem1  34687