Theorem eldif 3986

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
eldif	⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Proof of Theorem eldif

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3509	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3509	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2832	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2832	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 318	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 631	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3979	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3696	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979

This theorem is referenced by:  eldifd  3987  eldifad  3988  eldifbd  3989  elneeldif  3990  velcomp  3991  difeqri  4151  nfdif  4152  eldifi  4154  eldifn  4155  neldif  4157  difdif  4158  ddif  4164  ssconb  4165  sscon  4166  ssdif  4167  raldifb  4172  elsymdif  4277  dfss4  4288  dfun2  4289  dfin2  4290  difin  4291  indifdi  4313  undif3  4319  difin2  4320  ssdif0  4389  difin0ss  4396  inssdif0  4397  reldisj  4476  disj3  4477  undif4  4490  pssnel  4494  inundif  4502  ssundif  4511  eldifpr  4680  elpwunsn  4707  eldiftp  4710  eldifsn  4811  difprsnss  4824  iundif2  5097  iindif1  5098  iindif2  5100  disjss3  5165  brdif  5219  dffr6  5655  difopab  5854  difopabOLD  5855  intirr  6150  cnvdif  6175  difxp  6195  xpdifid  6199  frpoind  6374  wfiOLD  6383  ordunidif  6444  onmindif  6487  imadif  6662  dffv2  7017  eldifpw  7803  releldmdifi  8086  funeldmdif  8089  xpord2pred  8186  xpord2indlem  8188  ressuppssdif  8226  extmptsuppeq  8229  suppss  8235  suppssr  8236  suppssrg  8237  suppss2  8241  suppofssd  8244  suppcoss  8248  ondif2  8558  oelim2  8651  eldifsucnn  8720  boxcutc  8999  brsdom  9035  brsdom2  9163  php3  9275  php3OLD  9287  unblem1  9356  unfilem1  9371  elfi2  9483  dfsup2  9513  ordtypelem7  9593  ssttrcl  9784  ttrcltr  9785  dmttrcl  9790  frind  9819  kmlem4  10223  ackbij1lem18  10305  infpssr  10377  isf34lem4  10446  fin17  10463  fin67  10464  dffin7-2  10467  fin1a2lem6  10474  axcclem  10526  pwfseqlem3  10729  grothprim  10903  xrlenlt  11355  nzadd  12691  irradd  13038  irrmul  13039  difreicc  13544  modirr  13993  hashinf  14384  sumss  15772  fsumss  15773  prodss  15995  fprodss  15996  fprodn0f  16039  rpnnen2lem12  16273  dvdsaddre2b  16355  sumeven  16435  bitscmp  16484  lcmfunsnlem2  16687  iserodd  16882  prmodvdslcmf  17094  symgfix2  19458  pmtrdifellem4  19521  sylow2alem2  19660  efgsfo  19781  gsumval3  19949  gsum2dlem1  20012  gsum2dlem2  20013  ablfac1eu  20117  gsumdixp  20342  isnirred  20446  isirred2  20447  irredn0  20449  0ringdif  20553  0ring1eq0  20559  lsppratlem1  21172  lbsextlem2  21184  xrsmgmdifsgrp  21444  psgnodpm  21629  mplsubrglem  22047  mplcoe1  22078  mplcoe5  22081  opsrtoslem2  22103  symgmatr01lem  22680  elcls  23102  isclo  23116  maxlp  23176  restntr  23211  isreg2  23406  cmpcld  23431  hausdiag  23674  txkgen  23681  kqcldsat  23762  ufinffr  23958  fin1aufil  23961  alexsublem  24073  alexsubALTlem3  24078  ptcmplem5  24085  blcld  24539  shftmbl  25592  vitalilem4  25665  vitalilem5  25666  vitali  25667  mbfeqalem1  25695  itg1val2  25738  itg10a  25765  itg1ge0a  25766  mbfi1fseqlem4  25773  itg2uba  25798  itg2splitlem  25803  itg2monolem1  25805  itg2cnlem1  25816  itg2cnlem2  25817  itgss  25867  dvtaylp  26430  pserdvlem2  26490  ellogdm  26699  relogbcxp  26846  cxplogb  26847  logbmpt  26849  atandm  26937  atans2  26992  eldmgm  27083  igamgam  27110  igamf  27112  igamcl  27113  lgam1  27125  gam1  27126  wilthlem2  27130  basellem3  27144  fsumvma  27275  dchrelbas2  27299  dchreq  27320  dchrsum  27331  gausslemma2dlem4  27431  2sqreultblem  27510  dchrisum0fno1  27573  rplogsum  27589  newbday  27958  sltlpss  27963  islnopp  28765  frgrncvvdeq  30341  fusgr2wsp2nb  30366  eleigvec  31989  strlem1  32282  strlem5  32287  hstrlem5  32295  difrab2  32526  nfpconfp  32651  suppiniseg  32698  suppss3  32738  fsuppcurry1  32739  fsuppcurry2  32740  xrdifh  32785  nndiffz1  32791  ist0cld  33779  ordtconnlem1  33870  esumpinfval  34037  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemb  34333  eulerpartlemf  34335  eulerpartlemt  34336  eulerpartlemgh  34343  ballotlemodife  34462  ballotth  34502  reprdifc  34604  hgt750lemb  34633  elmrsubrn  35488  mrsubvrs  35490  dftr6  35713  dffr5  35716  brsset  35853  dfon3  35856  ellimits  35874  dffun10  35878  elfuns  35879  fullfunfv  35911  dfrecs2  35914  dfrdg4  35915  dfint3  35916  hfext  36147  onsucsuccmpi  36409  bj-rest10b  37055  difunieq  37340  pibt2  37383  iundif1  37554  lindsadd  37573  poimirlem2  37582  poimirlem11  37591  poimirlem12  37592  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  poimirlem30  37610  itg2addnclem  37631  ftc1anclem5  37657  areacirc  37673  fdc  37705  isfldidl  38028  opelvvdif  38215  iswatN  39951  dochsnkrlem1  41426  unitscyglem4  42155  selvcllem5  42537  selvvvval  42540  fsuppssindlem1  42546  ellz1  42723  pellexlem4  42788  pellexlem5  42789  ordeldif  43220  ordeldifsucon  43221  ordeldif1o  43222  cantnfresb  43286  cantnf2  43287  oadif1lem  43341  oadif1  43342  infordmin  43494  minregex  43496  pwinfig  43523  elnonrel  43547  sqrtcvallem1  43593  clsk3nimkb  44002  ntrclselnel1  44019  ntrneiel2  44048  ntrneik4w  44062  undif3VD  44853  iindif2f  45065  limcrecl  45550  icccncfext  45808  dvmptfprodlem  45865  stoweidlem26  45947  stoweidlem39  45960  stoweidlem52  45973  fourierdlem42  46070  etransclem18  46173  etransclem46  46201  ovolval4lem1  46570  requad01  47495  dfnbgr6  47729  lindslinindsimp1  48186  dignn0fr  48335