Theorem eldif 3486

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 3122	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 3122	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 465	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2539	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2539	. . . . 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 3479	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3252	. 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 1379   e. wcel 1767   _Vcvv 3113   \ cdif 3473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479

This theorem is referenced by:  eldifd  3487  eldifad  3488  eldifbd  3489  difeqri  3624  eldifi  3626  eldifn  3627  neldif  3629  difdif  3630  ddif  3636  ssconb  3637  sscon  3638  ssdif  3639  raldifb  3644  dfss4  3732  dfun2  3733  dfin2  3734  difin  3735  indifdir  3754  undif3  3759  difin2  3760  symdif2  3764  dfnul2  3787  reldisj  3870  disj3  3871  undif4  3883  ssdif0  3885  pssnel  3892  difin0ss  3893  inssdif0  3894  inundif  3905  ssundif  3910  eldifpr  4044  elpwunsn  4068  eldiftp  4070  eldifsn  4152  difprsnss  4162  iundif2  4392  iindif2  4394  disjss3  4446  brdif  4497  ordunidif  4926  onmindif  4967  difopab  5134  intirr  5385  cnvdif  5412  difxp  5431  xpdifid  5435  imadif  5663  dffv2  5940  suppssOLD  6014  suppssrOLD  6015  suppss2OLD  6514  eldifpw  6596  ressuppssdif  6921  extmptsuppeq  6924  suppss  6930  suppssr  6931  suppss2  6934  ondif2  7152  oelim2  7244  boxcutc  7512  brsdom  7538  brsdom2  7641  php3  7703  unblem1  7772  unfilem1  7784  elfi2  7874  dfsup2  7902  dfsup2OLD  7903  ordtypelem7  7949  kmlem4  8533  ackbij1lem18  8617  infpssr  8688  isf34lem4  8757  fin17  8774  fin67  8775  dffin7-2  8778  fin1a2lem6  8785  axcclem  8837  pwfseqlem3  9038  grothprim  9212  xrlenlt  9652  irradd  11206  irrmul  11207  difreicc  11652  modirr  12025  hashinf  12378  sumss  13509  fsumss  13510  rpnnen2  13820  bitscmp  13947  iserodd  14218  symgfix2  16246  pmtrdifellem4  16310  sylow2alem2  16444  efgsfo  16563  gsumval3OLD  16711  gsumval3  16714  gsum2dlem1  16800  gsum2dlem2  16801  gsum2dOLD  16803  ablfac1eu  16926  gsumdixpOLD  17058  gsumdixp  17059  isnirred  17150  isirred2  17151  irredn0  17153  lsppratlem1  17593  lbsextlem2  17605  mplsubrglem  17899  mplsubrglemOLD  17900  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  opsrtoslem2  17948  psgnodpm  18419  symgmatr01lem  18950  elcls  19368  isclo  19382  maxlp  19442  restntr  19477  isreg2  19672  cmpcld  19696  hausdiag  19909  txkgen  19916  kqcldsat  19997  ufinffr  20193  fin1aufil  20196  alexsublem  20307  alexsubALTlem3  20312  ptcmplem5  20319  blcld  20771  shftmbl  21712  vitalilem4  21783  vitalilem5  21784  vitali  21785  mbfeqalem  21812  itg1val2  21854  itg10a  21880  itg1ge0a  21881  mbfi1fseqlem4  21888  itg2uba  21913  itg2splitlem  21918  itg2monolem1  21920  itg2cnlem1  21931  itg2cnlem2  21932  itgss  21981  dvtaylp  22527  pserdvlem2  22585  ellogdm  22776  atandm  22963  atans2  23018  wilthlem2  23099  basellem3  23112  fsumvma  23244  dchrelbas2  23268  dchreq  23289  dchrsum  23300  dchrisum0fno1  23452  rplogsum  23468  isusgra0  24051  usgraop  24054  nbcusgra  24167  frgraunss  24699  frgrancvvdeqlem3  24737  frgrancvvdeqlem9  24746  frgrawopreglem3  24751  frgrawopreglem4  24752  frgrawopreg  24754  usg2spot2nb  24770  eleigvec  26580  strlem1  26873  strlem5  26878  hstrlem5  26886  suppss2f  27178  suppss3  27250  xrdifh  27287  nndiffz1  27292  ordtconlem1  27570  esumpinfval  27747  eulerpartlems  27967  eulerpartlemgc  27969  eulerpartlemb  27975  eulerpartlemf  27977  eulerpartlemt  27978  eulerpartlemgh  27985  ballotlemodife  28104  ballotth  28144  eldmgm  28232  igamgam  28259  igamf  28261  igamcl  28262  lgam1  28274  gam1  28275  prodss  28684  fprodss  28685  dftr6  28784  dffr5  28787  wfi  28892  frind  28928  elsymdif  29078  brsset  29144  dfon3  29147  ellimits  29165  dffun10  29169  elfuns  29170  fullfunfv  29202  dfrdg4  29205  tfrqfree  29206  dfint3  29207  hfext  29445  onsucsuccmpi  29513  iundif1  29642  dvtanlem  29669  itg2addnclem  29671  ftc1anclem5  29699  areacirc  29717  fdc  29869  isfldidl  30096  ellz1  30332  pellexlem4  30400  pellexlem5  30401  compel  30953  icoiccdif  31156  limciccioolb  31191  limcrecl  31199  limcicciooub  31207  lptre2pt  31210  icccncfext  31254  cncfiooicclem1  31260  stoweidlem26  31354  stoweidlem39  31367  stoweidlem52  31380  dirkercncflem2  31432  fourierdlem42  31477  fourierdlem62  31497  fourierdlem103  31538  fourierdlem104  31539  uhgraedgrnv  31844  lindslinindsimp1  32157  undif3VD  32780  iswatN  34808  dochsnkrlem1  36284