Theorem eldif 4052

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 3475	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3475	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2852	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2852	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 4050	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3637	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050

This theorem is used by:  eldifd  4053  eldifad  4054  eldifbd  4055  elneeldif  4056  velcomp  4057  difeqri  4068  nfdif  4069  eldifi  4070  eldifn  4071  neldif  4073  difdif  4074  ssconb  4081  sscon  4082  ssdif  4083  raldifb  4088  elsymdif  4206  dfss4  4217  dfun2  4218  dfin2  4219  difin  4220  indifdi  4242  undif3  4248  difin2  4249  ssdif0  4317  difin0ss  4324  inssdif0OLD  4326  reldisj  4409  disj3  4410  undif4  4423  pssnel  4427  inundif  4438  ssundif  4446  eldifpr  4620  elpwunsn  4646  eldiftp  4649  eldifsn  4750  difprsnss  4764  iundif2  5037  iindif1  5040  iindif2  5042  disjss3  5107  brdif  5164  dffr6  5614  difopab  5818  intirr  6130  cnvdif  6152  difxp  6173  xpdifid  6177  xpdifcnvepel  6178  frpoind  6371  ordunidif  6439  onmindif  6483  imadif  6654  dffv2  7011  eldifpw  7814  releldmdifi  8091  funeldmdif  8094  xpord2pred  8199  xpord2indlem  8201  ressuppssdif  8240  extmptsuppeq  8243  suppss  8249  suppssr  8250  suppssrg  8251  suppss2  8255  suppofssd  8258  suppcoss  8262  ondif2  8548  oelim2  8642  eldifsucnn  8711  boxcutc  9007  brsdom  9039  brsdom2  9158  php3  9262  unblem1  9322  unfilem1  9335  elfi2  9443  dfsup2  9473  ordtypelem7  9555  ssttrcl  9753  ttrcltr  9754  dmttrcl  9759  frind  9791  kmlem4  10271  ackbij1lem18  10353  infpssr  10425  isf34lem4  10494  fin17  10511  fin67  10512  dffin7-2  10515  fin1a2lem6  10522  axcclem  10574  pwfseqlem3  10784  grothprim  10958  xrlenlt  11413  nzadd  12784  irradd  13141  irrmul  13142  difreicc  13655  fzdif1  13779  modirr  14125  hashinf  14520  sumss  15934  fsumss  15935  prodss  16158  fprodss  16159  fprodn0f  16202  rpnnen2lem12  16437  dvdsaddre2b  16521  sumeven  16601  bitscmp  16652  lcmfunsnlem2  16859  iserodd  17057  prmodvdslcmf  17269  chnccat  18850  symgfix2  19681  pmtrdifellem4  19744  sylow2alem2  19883  efgsfo  20004  gsumval3  20172  gsum2dlem1  20235  gsum2dlem2  20236  ablfac1eu  20340  gsumdixp  20599  isnirred  20701  isirred2  20702  irredn0  20704  0ringdif  20829  0ring1eq0  20836  isdrng3lem2  21057  lsppratlem1  21476  lbsextlem2  21488  xrsmgmdifsgrp  21767  psgnodpm  21949  mplsubrglem  22366  mplcoe1  22401  mplcoe5  22404  opsrtoslem2  22420  selvcllem5  22503  selvvvval  22506  symgmatr01lem  23023  elcls  23446  isclo  23460  maxlp  23520  restntr  23555  isreg2  23750  cmpcld  23775  hausdiag  24019  txkgen  24026  kqcldsat  24107  ufinffr  24303  fin1aufil  24306  alexsublem  24418  alexsubALTlem3  24423  ptcmplem5  24430  blcld  24879  shftmbl  25914  vitalilem4  25987  vitalilem5  25988  vitali  25989  mbfeqalem1  26017  itg1val2  26060  itg10a  26086  itg1ge0a  26087  mbfi1fseqlem4  26094  itg2uba  26119  itg2splitlem  26124  itg2monolem1  26126  itg2cnlem1  26137  itg2cnlem2  26138  itgss  26187  dvtaylp  26754  pserdvlem2  26812  ellogdm  27024  relogbcxp  27170  cxplogb  27171  logbmpt  27173  atandm  27261  atans2  27316  eldmgm  27406  igamgam  27433  igamf  27435  igamcl  27436  lgam1  27448  gam1  27449  wilthlem2  27453  basellem3  27467  fsumvma  27597  dchrelbas2  27621  dchreq  27642  dchrsum  27653  gausslemma2dlem4  27753  2sqreultblem  27832  dchrisum0fno1  27895  rplogsum  27911  newbday  28345  ltslpss  28351  islnopp  29272  frgrncvvdeq  30967  fusgr2wsp2nb  30992  eleigvec  32616  strlem1  32909  strlem5  32914  hstrlem5  32922  difrab2  33193  nfpconfp  33324  fdifsupp  33375  suppiniseg  33376  suppss3  33411  fsuppcurry1  33412  fsuppcurry2  33413  xrdifh  33468  nndiffz1  33474  elrgspnsubrunlem2  33908  ist0cld  34576  ordtconnlem1  34667  esumpinfval  34816  eulerpartlems  35103  eulerpartlemgc  35105  eulerpartlemb  35111  eulerpartlemf  35113  eulerpartlemt  35114  eulerpartlemgh  35121  ballotlemodife  35241  ballotth  35281  reprdifc  35367  hgt750lemb  35396  onvf1od  36076  elmrsubrn  36493  mrsubvrs  36495  dftr6  36731  brsset  36866  dfon3  36869  ellimits  36887  dffun10  36891  elfuns  36892  fullfunfv  36926  dfrecs2  36929  dfrdg4  36930  dfint3  36931  hfext  37149  onsucsuccmpi  37446  bj-rest10b  38280  difunieq  38565  pibt2  38608  iundif1  38790  lindsadd  38804  poimirlem2  38808  poimirlem11  38817  poimirlem12  38818  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  poimirlem30  38836  itg2addnclem  38857  ftc1anclem5  38883  areacirc  38899  fdc  38945  isfldidl  39268  opelvvdif  39462  iswatN  41317  dochsnkrlem1  42792  unitscyglem4  43514  redvmptabs  43677  fsuppssindlem1  43885  ellz1  44044  pellexlem4  44105  pellexlem5  44106  ordeldif  44521  ordeldifsucon  44522  ordeldif1o  44523  cantnfresb  44587  cantnf2  44588  oadif1lem  44642  oadif1  44643  infordmin  44794  minregex  44796  pwinfig  44823  elnonrel  44847  sqrtcvallem1  44892  clsk3nimkb  45301  ntrclselnel1  45318  ntrneiel2  45347  ntrneik4w  45361  undif3VD  46124  iindif2f  46448  limcrecl  46914  icccncfext  47170  dvmptfprodlem  47227  stoweidlem26  47309  stoweidlem39  47322  stoweidlem52  47335  fourierdlem42  47432  etransclem18  47535  etransclem46  47563  ovolval4lem1  47932  requad01  48992  dfnbgr6  49228  lindslinindsimp1  49900  dignn0fr  50044