Theorem eldif 3909

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 3472	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3472	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2849	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3902	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3634	. 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 2145  Vcvv 3451   ∖ cdif 3896

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902

This theorem is used by:  eldifd  3910  eldifad  3911  eldifbd  3912  elneeldif  3913  velcomp  3914  difeqri  4076  nfdif  4077  eldifi  4078  eldifn  4079  neldif  4081  difdif  4082  ssconb  4089  sscon  4090  ssdif  4091  raldifb  4096  elsymdif  4204  dfss4  4215  dfun2  4216  dfin2  4217  difin  4218  indifdi  4240  undif3  4246  difin2  4247  ssdif0  4314  difin0ss  4321  inssdif0OLD  4323  reldisj  4406  disj3  4407  undif4  4420  pssnel  4424  inundif  4435  ssundif  4443  eldifpr  4619  elpwunsn  4645  eldiftp  4648  eldifsn  4748  difprsnss  4762  iundif2  5032  iindif1  5035  iindif2  5037  disjss3  5102  brdif  5158  dffr6  5607  difopab  5808  intirr  6112  cnvdif  6134  difxp  6155  xpdifid  6159  xpdifcnvepel  6160  frpoind  6345  ordunidif  6413  onmindif  6457  imadif  6624  dffv2  6980  eldifpw  7782  releldmdifi  8056  funeldmdif  8059  xpord2pred  8162  xpord2indlem  8164  ressuppssdif  8202  extmptsuppeq  8205  suppss  8211  suppssr  8212  suppssrg  8213  suppss2  8217  suppofssd  8220  suppcoss  8224  ondif2  8510  oelim2  8604  eldifsucnn  8673  boxcutc  8969  brsdom  9001  brsdom2  9120  php3  9224  unblem1  9284  unfilem1  9297  elfi2  9406  dfsup2  9436  ordtypelem7  9518  ssttrcl  9716  ttrcltr  9717  dmttrcl  9722  frind  9754  kmlem4  10232  ackbij1lem18  10314  infpssr  10386  isf34lem4  10455  fin17  10472  fin67  10473  dffin7-2  10476  fin1a2lem6  10483  axcclem  10535  pwfseqlem3  10745  grothprim  10919  xrlenlt  11374  nzadd  12744  irradd  13101  irrmul  13102  difreicc  13615  fzdif1  13739  modirr  14085  hashinf  14479  sumss  15890  fsumss  15891  prodss  16114  fprodss  16115  fprodn0f  16158  rpnnen2lem12  16393  dvdsaddre2b  16477  sumeven  16557  bitscmp  16608  lcmfunsnlem2  16815  iserodd  17013  prmodvdslcmf  17225  chnccat  18800  symgfix2  19630  pmtrdifellem4  19693  sylow2alem2  19832  efgsfo  19953  gsumval3  20121  gsum2dlem1  20184  gsum2dlem2  20185  ablfac1eu  20289  gsumdixp  20548  isnirred  20650  isirred2  20651  irredn0  20653  0ringdif  20778  0ring1eq0  20785  isdrng3lem2  21006  lsppratlem1  21425  lbsextlem2  21437  xrsmgmdifsgrp  21715  psgnodpm  21894  mplsubrglem  22311  mplcoe1  22346  mplcoe5  22349  opsrtoslem2  22365  selvcllem5  22448  selvvvval  22451  symgmatr01lem  22968  elcls  23391  isclo  23405  maxlp  23465  restntr  23500  isreg2  23695  cmpcld  23720  hausdiag  23964  txkgen  23971  kqcldsat  24052  ufinffr  24248  fin1aufil  24251  alexsublem  24363  alexsubALTlem3  24368  ptcmplem5  24375  blcld  24824  shftmbl  25859  vitalilem4  25932  vitalilem5  25933  vitali  25934  mbfeqalem1  25962  itg1val2  26005  itg10a  26031  itg1ge0a  26032  mbfi1fseqlem4  26039  itg2uba  26064  itg2splitlem  26069  itg2monolem1  26071  itg2cnlem1  26082  itg2cnlem2  26083  itgss  26132  dvtaylp  26697  pserdvlem2  26755  ellogdm  26967  relogbcxp  27113  cxplogb  27114  logbmpt  27116  atandm  27204  atans2  27259  eldmgm  27349  igamgam  27376  igamf  27378  igamcl  27379  lgam1  27391  gam1  27392  wilthlem2  27396  basellem3  27410  fsumvma  27540  dchrelbas2  27564  dchreq  27585  dchrsum  27596  gausslemma2dlem4  27696  2sqreultblem  27775  dchrisum0fno1  27838  rplogsum  27854  newbday  28288  ltslpss  28294  islnopp  29215  frgrncvvdeq  30910  fusgr2wsp2nb  30935  eleigvec  32559  strlem1  32852  strlem5  32857  hstrlem5  32865  difrab2  33094  nfpconfp  33226  fdifsupp  33278  suppiniseg  33279  suppss3  33315  fsuppcurry1  33316  fsuppcurry2  33317  xrdifh  33372  nndiffz1  33378  elrgspnsubrunlem2  33809  ist0cld  34465  ordtconnlem1  34556  esumpinfval  34705  eulerpartlems  34992  eulerpartlemgc  34994  eulerpartlemb  35000  eulerpartlemf  35002  eulerpartlemt  35003  eulerpartlemgh  35010  ballotlemodife  35130  ballotth  35170  reprdifc  35256  hgt750lemb  35285  onvf1od  35886  elmrsubrn  36285  mrsubvrs  36287  dftr6  36516  brsset  36651  dfon3  36654  ellimits  36672  dffun10  36676  elfuns  36677  fullfunfv  36711  dfrecs2  36714  dfrdg4  36715  dfint3  36716  hfext  36934  onsucsuccmpi  37231  bj-rest10b  38010  difunieq  38297  pibt2  38340  iundif1  38522  lindsadd  38536  poimirlem2  38540  poimirlem11  38549  poimirlem12  38550  poimirlem18  38556  poimirlem21  38559  poimirlem22  38560  poimirlem30  38568  itg2addnclem  38589  ftc1anclem5  38615  areacirc  38631  fdc  38679  isfldidl  39002  opelvvdif  39196  iswatN  41051  dochsnkrlem1  42526  unitscyglem4  43248  redvmptabs  43411  fsuppssindlem1  43619  ellz1  43777  pellexlem4  43838  pellexlem5  43839  ordeldif  44259  ordeldifsucon  44260  ordeldif1o  44261  cantnfresb  44325  cantnf2  44326  oadif1lem  44380  oadif1  44381  infordmin  44532  minregex  44534  pwinfig  44561  elnonrel  44585  sqrtcvallem1  44630  clsk3nimkb  45039  ntrclselnel1  45056  ntrneiel2  45085  ntrneik4w  45099  undif3VD  45863  iindif2f  46174  limcrecl  46640  icccncfext  46896  dvmptfprodlem  46953  stoweidlem26  47035  stoweidlem39  47048  stoweidlem52  47061  fourierdlem42  47158  etransclem18  47261  etransclem46  47289  ovolval4lem1  47658  requad01  48718  dfnbgr6  48954  lindslinindsimp1  49568  dignn0fr  49712