Theorem eldif 3584

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 3212	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 3212	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 481	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2689	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2689	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 308	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 747	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3577	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3353	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 368	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   _Vcvv 3200   \ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577

This theorem is referenced by:  eldifd  3585  eldifad  3586  eldifbd  3587  difeqri  3730  eldifi  3732  eldifn  3733  neldif  3735  difdif  3736  ddif  3742  ssconb  3743  sscon  3744  ssdif  3745  raldifb  3750  elsymdif  3849  symdif2  3852  dfss4  3858  dfun2  3859  dfin2  3860  difin  3861  indifdir  3883  undif3  3888  undif3OLD  3889  difin2  3890  dfnul2  3917  ssdif0  3942  difin0ss  3946  inssdif0  3947  reldisj  4020  disj3  4021  undif4  4035  pssnel  4039  inundif  4046  ssundif  4052  eldifpr  4204  elpwunsn  4224  eldiftp  4228  eldifsn  4317  difprsnss  4329  iundif2  4587  iindif2  4589  disjss3  4652  brdif  4705  difopab  5253  intirr  5514  cnvdif  5539  difxp  5558  xpdifid  5562  wfi  5713  ordunidif  5773  onmindif  5815  imadif  5973  dffv2  6271  eldifpw  6976  ressuppssdif  7316  extmptsuppeq  7319  suppss  7325  suppssr  7326  suppss2  7329  ondif2  7582  oelim2  7675  boxcutc  7951  brsdom  7978  brsdom2  8084  php3  8146  unblem1  8212  unfilem1  8224  elfi2  8320  dfsup2  8350  ordtypelem7  8429  kmlem4  8975  ackbij1lem18  9059  infpssr  9130  isf34lem4  9199  fin17  9216  fin67  9217  dffin7-2  9220  fin1a2lem6  9227  axcclem  9279  pwfseqlem3  9482  grothprim  9656  xrlenlt  10103  nzadd  11425  irradd  11812  irrmul  11813  difreicc  12304  modirr  12741  hashinf  13122  sumss  14455  fsumss  14456  prodss  14677  fprodss  14678  fprodn0f  14722  rpnnen2lem12  14954  dvdsaddre2b  15029  sumeven  15110  bitscmp  15160  lcmfunsnlem2  15353  iserodd  15540  prmodvdslcmf  15751  symgfix2  17836  pmtrdifellem4  17899  sylow2alem2  18033  efgsfo  18152  gsumval3  18308  gsum2dlem1  18369  gsum2dlem2  18370  ablfac1eu  18472  gsumdixp  18609  isnirred  18700  isirred2  18701  irredn0  18703  lsppratlem1  19147  lbsextlem2  19159  mplsubrglem  19439  mplcoe1  19465  mplcoe5  19468  opsrtoslem2  19485  xrsmgmdifsgrp  19783  psgnodpm  19934  symgmatr01lem  20459  elcls  20877  isclo  20891  maxlp  20951  restntr  20986  isreg2  21181  cmpcld  21205  hausdiag  21448  txkgen  21455  kqcldsat  21536  ufinffr  21733  fin1aufil  21736  alexsublem  21848  alexsubALTlem3  21853  ptcmplem5  21860  blcld  22310  shftmbl  23306  vitalilem4  23380  vitalilem5  23381  vitali  23382  mbfeqalem  23409  itg1val2  23451  itg10a  23477  itg1ge0a  23478  mbfi1fseqlem4  23485  itg2uba  23510  itg2splitlem  23515  itg2monolem1  23517  itg2cnlem1  23528  itg2cnlem2  23529  itgss  23578  dvtaylp  24124  pserdvlem2  24182  ellogdm  24385  relogbcxp  24523  cxplogb  24524  logbmpt  24526  atandm  24603  atans2  24658  eldmgm  24748  igamgam  24775  igamf  24777  igamcl  24778  lgam1  24790  gam1  24791  wilthlem2  24795  basellem3  24809  fsumvma  24938  dchrelbas2  24962  dchreq  24983  dchrsum  24994  gausslemma2dlem4  25094  dchrisum0fno1  25200  rplogsum  25216  islnopp  25631  frgrncvvdeq  27173  fusgr2wsp2nb  27198  eleigvec  28816  strlem1  29109  strlem5  29114  hstrlem5  29122  difrab2  29339  suppss3  29502  xrdifh  29542  nndiffz1  29548  ordtconnlem1  29970  esumpinfval  30135  eulerpartlems  30422  eulerpartlemgc  30424  eulerpartlemb  30430  eulerpartlemf  30432  eulerpartlemt  30433  eulerpartlemgh  30440  ballotlemodife  30559  ballotth  30599  reprdifc  30705  hgt750lemb  30734  elmrsubrn  31417  mrsubvrs  31419  dftr6  31640  dffr5  31643  frind  31740  brsset  31996  dfon3  31999  ellimits  32017  dffun10  32021  elfuns  32022  fullfunfv  32054  dfrecs2  32057  dfrdg4  32058  dfint3  32059  hfext  32290  onsucsuccmpi  32442  bj-rest10b  33042  iundif1  33383  poimirlem2  33411  poimirlem11  33420  poimirlem12  33421  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem30  33439  itg2addnclem  33461  ftc1anclem5  33489  areacirc  33505  fdc  33541  isfldidl  33867  opelvvdif  34023  iswatN  35280  dochsnkrlem1  36758  ellz1  37330  pellexlem4  37396  pellexlem5  37397  pwinfig  37866  elnonrel  37891  clsk3nimkb  38338  ntrclselnel1  38355  ntrneiel2  38384  ntrneik4w  38398  compel  38641  undif3VD  39118  limcrecl  39861  icccncfext  40100  dvmptfprodlem  40159  stoweidlem26  40243  stoweidlem39  40256  stoweidlem52  40269  fourierdlem42  40366  etransclem18  40469  etransclem46  40497  ovolval4lem1  40863  0ringdif  41870  0ring1eq0  41872  lindslinindsimp1  42246  dignn0fr  42395