Theorem eldif 3445

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 3085	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 3085	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 465	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2526	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2526	. . . . 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 3438	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 3213	. 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 1370   e. wcel 1758   _Vcvv 3076   \ cdif 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-dif 3438

This theorem is referenced by:  eldifd  3446  eldifad  3447  eldifbd  3448  difeqri  3583  eldifi  3585  eldifn  3586  neldif  3588  difdif  3589  ddif  3595  ssconb  3596  sscon  3597  ssdif  3598  raldifb  3603  dfss4  3691  dfun2  3692  dfin2  3693  difin  3694  indifdir  3713  undif3  3718  difin2  3719  symdif2  3723  dfnul2  3746  reldisj  3829  disj3  3830  undif4  3842  ssdif0  3844  pssnel  3851  difin0ss  3852  inssdif0  3853  inundif  3864  ssundif  3869  eldifpr  4001  elpwunsn  4024  eldiftp  4026  eldifsn  4107  difprsnss  4116  iundif2  4344  iindif2  4346  disjss3  4398  brdif  4449  ordunidif  4874  onmindif  4915  difopab  5078  intirr  5323  cnvdif  5350  difxp  5369  xpdifid  5373  imadif  5600  dffv2  5872  suppssOLD  5944  suppssrOLD  5945  suppss2OLD  6424  eldifpw  6497  ressuppssdif  6819  extmptsuppeq  6822  suppss  6828  suppssr  6829  suppss2  6832  ondif2  7051  oelim2  7143  boxcutc  7415  brsdom  7441  brsdom2  7544  php3  7606  unblem1  7674  unfilem1  7686  elfi2  7774  dfsup2  7802  dfsup2OLD  7803  ordtypelem7  7848  kmlem4  8432  ackbij1lem18  8516  infpssr  8587  isf34lem4  8656  fin17  8673  fin67  8674  dffin7-2  8677  fin1a2lem6  8684  axcclem  8736  pwfseqlem3  8937  grothprim  9111  xrlenlt  9552  irradd  11087  irrmul  11088  difreicc  11533  modirr  11885  hashinf  12224  sumss  13318  fsumss  13319  rpnnen2  13625  bitscmp  13751  iserodd  14019  symgfix2  16039  pmtrdifellem4  16103  sylow2alem2  16237  efgsfo  16356  gsumval3OLD  16502  gsumval3  16505  gsum2dlem1  16582  gsum2dlem2  16583  gsum2dOLD  16585  ablfac1eu  16695  gsumdixpOLD  16822  gsumdixp  16823  isnirred  16914  isirred2  16915  irredn0  16917  lsppratlem1  17350  lbsextlem2  17362  mplsubrglem  17640  mplsubrglemOLD  17641  mplcoe1  17667  mplcoe5  17671  mplcoe2OLD  17673  opsrtoslem2  17689  psgnodpm  18142  symgmatr01lem  18590  elcls  18808  isclo  18822  maxlp  18882  restntr  18917  isreg2  19112  cmpcld  19136  hausdiag  19349  txkgen  19356  kqcldsat  19437  ufinffr  19633  fin1aufil  19636  alexsublem  19747  alexsubALTlem3  19752  ptcmplem5  19759  blcld  20211  shftmbl  21152  vitalilem4  21223  vitalilem5  21224  vitali  21225  mbfeqalem  21252  itg1val2  21294  itg10a  21320  itg1ge0a  21321  mbfi1fseqlem4  21328  itg2uba  21353  itg2splitlem  21358  itg2monolem1  21360  itg2cnlem1  21371  itg2cnlem2  21372  itgss  21421  dvtaylp  21967  pserdvlem2  22025  ellogdm  22216  atandm  22403  atans2  22458  wilthlem2  22539  basellem3  22552  fsumvma  22684  dchrelbas2  22708  dchreq  22729  dchrsum  22740  dchrisum0fno1  22892  rplogsum  22908  isusgra0  23426  nbcusgra  23522  eleigvec  25512  strlem1  25805  strlem5  25810  hstrlem5  25818  suppss2f  26104  suppss3  26177  xrdifh  26214  nndiffz1  26219  ordtconlem1  26498  esumpinfval  26666  eulerpartlems  26886  eulerpartlemgc  26888  eulerpartlemb  26894  eulerpartlemf  26896  eulerpartlemt  26897  eulerpartlemgh  26904  ballotlemodife  27023  ballotth  27063  eldmgm  27151  igamgam  27178  igamf  27180  igamcl  27181  lgam1  27193  gam1  27194  prodss  27603  fprodss  27604  dftr6  27703  dffr5  27706  wfi  27811  frind  27847  elsymdif  27997  brsset  28063  dfon3  28066  ellimits  28084  dffun10  28088  elfuns  28089  fullfunfv  28121  dfrdg4  28124  tfrqfree  28125  dfint3  28126  hfext  28364  onsucsuccmpi  28432  iundif1  28560  dvtanlem  28588  itg2addnclem  28590  ftc1anclem5  28618  areacirc  28636  fdc  28788  isfldidl  29015  ellz1  29252  pellexlem4  29320  pellexlem5  29321  compel  29841  stoweidlem26  29968  stoweidlem39  29981  stoweidlem52  29994  uhgraedgrnv  30420  frgraunss  30734  frgrancvvdeqlem3  30772  frgrancvvdeqlem9  30781  frgrawopreglem3  30786  frgrawopreglem4  30787  frgrawopreg  30789  usg2spot2nb  30805  lindslinindsimp1  31109  undif3VD  31935  iswatN  33961  dochsnkrlem1  35437