Theorem eldif 3876

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 3426	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3426	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 484	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2825	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2825	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 634	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3869	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3589	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 383	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  Vcvv 3408   ∖ cdif 3863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-dif 3869

This theorem is referenced by:  eldifd  3877  eldifad  3878  eldifbd  3879  elneeldif  3880  velcomp  3881  difeqri  4039  eldifi  4041  eldifn  4042  neldif  4044  difdif  4045  ddif  4051  ssconb  4052  sscon  4053  ssdif  4054  raldifb  4059  elsymdif  4162  dfss4  4173  dfun2  4174  dfin2  4175  difin  4176  indifdi  4198  indifdirOLD  4200  undif3  4205  difin2  4206  ssdif0  4278  difin0ss  4283  inssdif0  4284  reldisj  4366  reldisjOLD  4367  disj3  4368  undif4  4381  pssnel  4385  inundif  4393  ssundif  4399  eldifpr  4573  elpwunsn  4599  eldiftp  4602  eldifsn  4700  difprsnss  4712  iundif2  4982  iindif1  4983  iindif2  4985  disjss3  5052  brdif  5106  difopab  5700  intirr  5983  cnvdif  6007  difxp  6027  xpdifid  6031  frpoind  6196  wfi  6203  ordunidif  6261  onmindif  6302  imadif  6464  dffv2  6806  eldifpw  7553  releldmdifi  7816  funeldmdif  7819  ressuppssdif  7927  extmptsuppeq  7930  suppss  7936  suppssOLD  7937  suppssr  7938  suppssrg  7939  suppss2  7942  suppofssd  7945  suppcoss  7949  ondif2  8229  oelim2  8323  boxcutc  8622  brsdom  8651  brsdom2  8770  php3  8832  unblem1  8923  unfilem1  8935  elfi2  9030  dfsup2  9060  ordtypelem7  9140  frind  9366  kmlem4  9767  ackbij1lem18  9851  infpssr  9922  isf34lem4  9991  fin17  10008  fin67  10009  dffin7-2  10012  fin1a2lem6  10019  axcclem  10071  pwfseqlem3  10274  grothprim  10448  xrlenlt  10898  nzadd  12225  irradd  12569  irrmul  12570  difreicc  13072  modirr  13515  hashinf  13901  sumss  15288  fsumss  15289  prodss  15509  fprodss  15510  fprodn0f  15553  rpnnen2lem12  15786  dvdsaddre2b  15868  sumeven  15948  bitscmp  15997  lcmfunsnlem2  16197  iserodd  16388  prmodvdslcmf  16600  symgfix2  18808  pmtrdifellem4  18871  sylow2alem2  19007  efgsfo  19129  gsumval3  19292  gsum2dlem1  19355  gsum2dlem2  19356  ablfac1eu  19460  gsumdixp  19627  isnirred  19718  isirred2  19719  irredn0  19721  lsppratlem1  20184  lbsextlem2  20196  xrsmgmdifsgrp  20400  psgnodpm  20550  mplsubrglem  20966  mplcoe1  20994  mplcoe5  20997  opsrtoslem2  21013  symgmatr01lem  21550  elcls  21970  isclo  21984  maxlp  22044  restntr  22079  isreg2  22274  cmpcld  22299  hausdiag  22542  txkgen  22549  kqcldsat  22630  ufinffr  22826  fin1aufil  22829  alexsublem  22941  alexsubALTlem3  22946  ptcmplem5  22953  blcld  23403  shftmbl  24435  vitalilem4  24508  vitalilem5  24509  vitali  24510  mbfeqalem1  24538  itg1val2  24581  itg10a  24608  itg1ge0a  24609  mbfi1fseqlem4  24616  itg2uba  24641  itg2splitlem  24646  itg2monolem1  24648  itg2cnlem1  24659  itg2cnlem2  24660  itgss  24709  dvtaylp  25262  pserdvlem2  25320  ellogdm  25527  relogbcxp  25668  cxplogb  25669  logbmpt  25671  atandm  25759  atans2  25814  eldmgm  25904  igamgam  25931  igamf  25933  igamcl  25934  lgam1  25946  gam1  25947  wilthlem2  25951  basellem3  25965  fsumvma  26094  dchrelbas2  26118  dchreq  26139  dchrsum  26150  gausslemma2dlem4  26250  2sqreultblem  26329  dchrisum0fno1  26392  rplogsum  26408  islnopp  26830  frgrncvvdeq  28392  fusgr2wsp2nb  28417  eleigvec  30038  strlem1  30331  strlem5  30336  hstrlem5  30344  difrab2  30564  nfpconfp  30686  suppiniseg  30740  suppss3  30779  fsuppcurry1  30780  fsuppcurry2  30781  xrdifh  30821  nndiffz1  30827  ist0cld  31497  ordtconnlem1  31588  esumpinfval  31753  eulerpartlems  32039  eulerpartlemgc  32041  eulerpartlemb  32047  eulerpartlemf  32049  eulerpartlemt  32050  eulerpartlemgh  32057  ballotlemodife  32176  ballotth  32216  reprdifc  32319  hgt750lemb  32348  elmrsubrn  33195  mrsubvrs  33197  eldifsucnn  33410  dftr6  33436  dffr5  33439  ssttrcl  33514  ttrcltr  33515  dmttrcl  33520  xpord2pred  33529  xpord2ind  33531  xpord3pred  33535  newbday  33819  sltlpss  33824  brsset  33928  dfon3  33931  ellimits  33949  dffun10  33953  elfuns  33954  fullfunfv  33986  dfrecs2  33989  dfrdg4  33990  dfint3  33991  hfext  34222  onsucsuccmpi  34369  bj-rest10b  34995  difunieq  35282  pibt2  35325  iundif1  35488  lindsadd  35507  poimirlem2  35516  poimirlem11  35525  poimirlem12  35526  poimirlem18  35532  poimirlem21  35535  poimirlem22  35536  poimirlem30  35544  itg2addnclem  35565  ftc1anclem5  35591  areacirc  35607  fdc  35640  isfldidl  35963  opelvvdif  36135  iswatN  37745  dochsnkrlem1  39220  selvval2lem5  39942  fsuppssindlem1  39990  ellz1  40292  pellexlem4  40357  pellexlem5  40358  infordmin  40824  pwinfig  40844  elnonrel  40869  sqrtcvallem1  40915  clsk3nimkb  41327  ntrclselnel1  41344  ntrneiel2  41373  ntrneik4w  41387  undif3VD  42175  limcrecl  42845  icccncfext  43103  dvmptfprodlem  43160  stoweidlem26  43242  stoweidlem39  43255  stoweidlem52  43268  fourierdlem42  43365  etransclem18  43468  etransclem46  43496  ovolval4lem1  43862  requad01  44746  0ringdif  45101  0ring1eq0  45103  lindslinindsimp1  45471  dignn0fr  45620