Theorem eldif 3290

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 2924	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2924	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 452	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2464	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2464	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 286	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 692	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3283	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3044	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 343	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   _Vcvv 2916   \ cdif 3277

This theorem is referenced by:  eldifd  3291  eldifad  3292  eldifbd  3293  difeqri  3427  eldifi  3429  eldifn  3430  neldif  3432  difdif  3433  ddif  3439  ssconb  3440  sscon  3441  ssdif  3442  raldifb  3447  dfss4  3535  dfun2  3536  dfin2  3537  difin  3538  indifdir  3557  undif3  3562  difin2  3563  symdif2  3567  dfnul2  3590  reldisj  3631  disj3  3632  undif4  3644  ssdif0  3646  pssnel  3653  difin0ss  3654  inssdif0  3655  inundif  3666  ssundif  3671  eldifsn  3887  difprsnss  3894  iundif2  4118  iindif2  4120  disjss3  4171  brdif  4220  ordunidif  4589  onmindif  4630  eldifpw  4714  elpwunsn  4716  difopab  4965  intirr  5211  cnvdif  5237  imadif  5487  dffv2  5755  suppss  5822  suppssr  5823  suppss2  6259  difxp  6339  ondif2  6705  oelim2  6797  boxcutc  7064  brsdom  7089  brsdom2  7190  php3  7252  unblem1  7318  unfilem1  7330  elfi2  7377  dfsup2  7405  dfsup2OLD  7406  ordtypelem7  7449  cantnfreslem  7587  kmlem4  7989  ackbij1lem18  8073  infpssr  8144  isf34lem4  8213  fin17  8230  fin67  8231  dffin7-2  8234  fin1a2lem6  8241  axcclem  8293  pwfseqlem3  8491  grothprim  8665  xrlenlt  9099  irradd  10554  irrmul  10555  difreicc  10984  modirr  11241  hashinf  11578  sumss  12473  fsumss  12474  rpnnen2  12780  bitscmp  12905  iserodd  13164  sylow2alem2  15207  efgsfo  15326  gsumval3  15469  gsum2d  15501  ablfac1eu  15586  gsumdixp  15670  isnirred  15760  isirred2  15761  irredn0  15763  lsppratlem1  16174  lbsextlem2  16186  mplsubrglem  16457  mplcoe1  16483  mplcoe2  16485  opsrtoslem2  16500  elcls  17092  isclo  17106  maxlp  17165  restntr  17200  isreg2  17395  cmpcld  17419  hausdiag  17630  txkgen  17637  kqcldsat  17718  ufinffr  17914  fin1aufil  17917  alexsublem  18028  alexsubALTlem3  18033  ptcmplem5  18040  blcld  18488  shftmbl  19386  vitalilem4  19456  vitalilem5  19457  vitali  19458  mbfeqalem  19487  itg1val2  19529  itg10a  19555  itg1ge0a  19556  mbfi1fseqlem4  19563  itg2uba  19588  itg2splitlem  19593  itg2monolem1  19595  itg2cnlem1  19606  itg2cnlem2  19607  itgss  19656  dvtaylp  20239  pserdvlem2  20297  ellogdm  20483  atandm  20669  atans2  20724  wilthlem2  20805  basellem3  20818  fsumvma  20950  dchrelbas2  20974  dchreq  20995  dchrsum  21006  dchrisum0fno1  21158  rplogsum  21174  isusgra0  21329  nbcusgra  21425  eleigvec  23413  strlem1  23706  strlem5  23711  hstrlem5  23719  suppss2f  24002  xrdifh  24096  eldifpr  24345  eldiftp  24346  esumpinfval  24416  sibfof  24607  ballotlemodife  24708  ballotth  24748  eldmgm  24759  igamgam  24786  igamf  24788  igamcl  24789  lgam1  24801  gam1  24802  prodss  25226  fprodss  25227  dftr6  25321  dffr5  25324  wfi  25421  frind  25457  elsymdif  25581  brsset  25643  dfon3  25646  ellimits  25664  elfuns  25668  fullfunfv  25700  dfrdg4  25703  tfrqfree  25704  hfext  26028  onsucsuccmpi  26097  itg2addnclem  26155  areacirc  26187  fdc  26339  isfldidl  26568  ellz1  26715  pellexlem4  26785  pellexlem5  26786  compel  27508  stoweidlem26  27642  stoweidlem39  27655  stoweidlem52  27668  uhgraedgrnv  28032  frgraunss  28099  frgrancvvdeqlem3  28135  frgrancvvdeqlem9  28144  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreg  28152  usg2spot2nb  28168  undif3VD  28703  iswatN  30476  dochsnkrlem1  31952

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283