Theorem eldif 3413

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 3053	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 3053	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 467	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2516	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2516	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 296	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 716	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3406	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3186	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 355	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   <-> wb 188   /\ wa 371   = wceq 1443   e. wcel 1886   _Vcvv 3044   \ cdif 3400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-dif 3406

This theorem is referenced by:  eldifd  3414  eldifad  3415  eldifbd  3416  difeqri  3552  eldifi  3554  eldifn  3555  neldif  3557  difdif  3558  ddif  3564  ssconb  3565  sscon  3566  ssdif  3567  raldifb  3572  elsymdif  3667  symdif2  3670  dfss4  3676  dfun2  3677  dfin2  3678  difin  3679  indifdir  3698  undif3  3703  difin2  3704  dfnul2  3732  reldisj  3807  disj3  3808  undif4  3820  ssdif0  3822  pssnel  3831  difin0ss  3832  inssdif0  3833  inundif  3844  ssundif  3850  eldifpr  3989  elpwunsn  4011  eldiftp  4014  eldifsn  4096  difprsnss  4106  iundif2  4344  iindif2  4346  disjss3  4400  brdif  4452  difopab  4965  intirr  5217  cnvdif  5241  difxp  5260  xpdifid  5264  wfi  5412  ordunidif  5470  onmindif  5511  imadif  5656  dffv2  5936  eldifpw  6600  ressuppssdif  6933  extmptsuppeq  6936  suppss  6942  suppssr  6943  suppss2  6946  ondif2  7201  oelim2  7293  boxcutc  7562  brsdom  7589  brsdom2  7693  php3  7755  unblem1  7820  unfilem1  7832  elfi2  7925  dfsup2  7955  ordtypelem7  8036  kmlem4  8580  ackbij1lem18  8664  infpssr  8735  isf34lem4  8804  fin17  8821  fin67  8822  dffin7-2  8825  fin1a2lem6  8832  axcclem  8884  pwfseqlem3  9082  grothprim  9256  xrlenlt  9696  irradd  11285  irrmul  11286  difreicc  11761  modirr  12157  hashinf  12517  sumss  13783  fsumss  13784  prodss  13994  fprodss  13995  fprodn0f  14038  rpnnen2  14271  bitscmp  14405  lcmfunsnlem2  14606  iserodd  14778  prmodvdslcmf  14998  prmordvdslcmfOLD  15012  prmordvdslcmsOLDOLD  15014  symgfix2  17050  pmtrdifellem4  17113  sylow2alem2  17263  efgsfo  17382  gsumval3  17534  gsum2dlem1  17595  gsum2dlem2  17596  ablfac1eu  17699  gsumdixp  17830  isnirred  17921  isirred2  17922  irredn0  17924  lsppratlem1  18363  lbsextlem2  18375  mplsubrglem  18656  mplcoe1  18682  mplcoe5  18685  opsrtoslem2  18701  xrsmgmdifsgrp  18998  psgnodpm  19149  symgmatr01lem  19671  elcls  20082  isclo  20096  maxlp  20156  restntr  20191  isreg2  20386  cmpcld  20410  hausdiag  20653  txkgen  20660  kqcldsat  20741  ufinffr  20937  fin1aufil  20940  alexsublem  21052  alexsubALTlem3  21057  ptcmplem5  21064  blcld  21513  shftmbl  22485  vitalilem4  22562  vitalilem5  22563  vitali  22564  mbfeqalem  22591  itg1val2  22635  itg10a  22661  itg1ge0a  22662  mbfi1fseqlem4  22669  itg2uba  22694  itg2splitlem  22699  itg2monolem1  22701  itg2cnlem1  22712  itg2cnlem2  22713  itgss  22762  dvtaylp  23318  pserdvlem2  23376  ellogdm  23577  relogbcxp  23715  cxplogb  23716  logbmpt  23718  atandm  23795  atans2  23850  eldmgm  23940  igamgam  23967  igamf  23969  igamcl  23970  lgam1  23982  gam1  23983  wilthlem2  23987  basellem3  24002  fsumvma  24134  dchrelbas2  24158  dchreq  24179  dchrsum  24190  dchrisum0fno1  24342  rplogsum  24358  islnopp  24774  isusgra0  25067  usgraop  25070  nbcusgra  25184  frgraunss  25716  frgrancvvdeqlem3  25753  frgrancvvdeqlem9  25762  frgrawopreglem3  25767  frgrawopreglem4  25768  frgrawopreg  25770  usg2spot2nb  25786  eleigvec  27603  strlem1  27896  strlem5  27901  hstrlem5  27909  suppss2fOLD  28230  suppss3  28305  xrdifh  28355  nndiffz1  28359  ordtconlem1  28723  esumpinfval  28887  eulerpartlems  29186  eulerpartlemgc  29188  eulerpartlemb  29194  eulerpartlemf  29196  eulerpartlemt  29197  eulerpartlemgh  29204  ballotlemodife  29323  ballotth  29363  ballotthOLD  29401  elmrsubrn  30151  mrsubvrs  30153  dftr6  30383  dffr5  30386  frind  30474  brsset  30649  dfon3  30652  ellimits  30670  dffun10  30674  elfuns  30675  fullfunfv  30707  dfrecs2  30710  dfrdg4  30711  dfint3  30712  hfext  30943  onsucsuccmpi  31096  iundif1  31920  poimirlem2  31935  poimirlem11  31944  poimirlem12  31945  poimirlem18  31951  poimirlem21  31954  poimirlem22  31955  poimirlem30  31963  dvtanlemOLD  31984  itg2addnclem  31986  ftc1anclem5  32014  areacirc  32030  fdc  32067  isfldidl  32294  iswatN  33553  dochsnkrlem1  35031  ellz1  35603  pellexlem4  35670  pellexlem5  35671  pwinfig  36159  elnonrel  36185  compel  36785  undif3VD  37273  limcrecl  37703  icccncfext  37759  dvmptfprodlem  37813  stoweidlem26  37880  stoweidlem39  37894  stoweidlem52  37907  fourierdlem42  38006  fourierdlem42OLD  38007  etransclem18  38111  etransclem46  38139  uhgraedgrnv  39650  0ringdif  39857  0ring1eq0  39859  lindslinindsimp1  40237  dignn0fr  40399