Theorem eldif 3898

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 3451	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3451	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2827	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2827	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 318	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 631	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3891	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3612	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 380	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  Vcvv 3433   ∖ cdif 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891

This theorem is referenced by:  eldifd  3899  eldifad  3900  eldifbd  3901  elneeldif  3902  velcomp  3903  difeqri  4060  eldifi  4062  eldifn  4063  neldif  4065  difdif  4066  ddif  4072  ssconb  4073  sscon  4074  ssdif  4075  raldifb  4080  elsymdif  4182  dfss4  4193  dfun2  4194  dfin2  4195  difin  4196  indifdi  4218  indifdirOLD  4220  undif3  4225  difin2  4226  ssdif0  4298  difin0ss  4303  inssdif0  4304  reldisj  4386  reldisjOLD  4387  disj3  4388  undif4  4401  pssnel  4405  inundif  4413  ssundif  4419  eldifpr  4594  elpwunsn  4620  eldiftp  4623  eldifsn  4721  difprsnss  4733  iundif2  5004  iindif1  5005  iindif2  5007  disjss3  5074  brdif  5128  dffr6  5548  difopab  5742  difopabOLD  5743  intirr  6028  cnvdif  6052  difxp  6072  xpdifid  6076  frpoind  6249  wfiOLD  6258  ordunidif  6318  onmindif  6359  imadif  6525  dffv2  6872  eldifpw  7627  releldmdifi  7895  funeldmdif  7898  ressuppssdif  8010  extmptsuppeq  8013  suppss  8019  suppssOLD  8020  suppssr  8021  suppssrg  8022  suppss2  8025  suppofssd  8028  suppcoss  8032  ondif2  8341  oelim2  8435  eldifsucnn  8503  boxcutc  8738  brsdom  8772  brsdom2  8893  php3  9004  php3OLD  9016  unblem1  9075  unfilem1  9087  elfi2  9182  dfsup2  9212  ordtypelem7  9292  ssttrcl  9482  ttrcltr  9483  dmttrcl  9488  frind  9517  kmlem4  9918  ackbij1lem18  10002  infpssr  10073  isf34lem4  10142  fin17  10159  fin67  10160  dffin7-2  10163  fin1a2lem6  10170  axcclem  10222  pwfseqlem3  10425  grothprim  10599  xrlenlt  11049  nzadd  12377  irradd  12722  irrmul  12723  difreicc  13225  modirr  13671  hashinf  14058  sumss  15445  fsumss  15446  prodss  15666  fprodss  15667  fprodn0f  15710  rpnnen2lem12  15943  dvdsaddre2b  16025  sumeven  16105  bitscmp  16154  lcmfunsnlem2  16354  iserodd  16545  prmodvdslcmf  16757  symgfix2  19033  pmtrdifellem4  19096  sylow2alem2  19232  efgsfo  19354  gsumval3  19517  gsum2dlem1  19580  gsum2dlem2  19581  ablfac1eu  19685  gsumdixp  19857  isnirred  19951  isirred2  19952  irredn0  19954  lsppratlem1  20418  lbsextlem2  20430  xrsmgmdifsgrp  20644  psgnodpm  20802  mplsubrglem  21219  mplcoe1  21247  mplcoe5  21250  opsrtoslem2  21272  symgmatr01lem  21811  elcls  22233  isclo  22247  maxlp  22307  restntr  22342  isreg2  22537  cmpcld  22562  hausdiag  22805  txkgen  22812  kqcldsat  22893  ufinffr  23089  fin1aufil  23092  alexsublem  23204  alexsubALTlem3  23209  ptcmplem5  23216  blcld  23670  shftmbl  24711  vitalilem4  24784  vitalilem5  24785  vitali  24786  mbfeqalem1  24814  itg1val2  24857  itg10a  24884  itg1ge0a  24885  mbfi1fseqlem4  24892  itg2uba  24917  itg2splitlem  24922  itg2monolem1  24924  itg2cnlem1  24935  itg2cnlem2  24936  itgss  24985  dvtaylp  25538  pserdvlem2  25596  ellogdm  25803  relogbcxp  25944  cxplogb  25945  logbmpt  25947  atandm  26035  atans2  26090  eldmgm  26180  igamgam  26207  igamf  26209  igamcl  26210  lgam1  26222  gam1  26223  wilthlem2  26227  basellem3  26241  fsumvma  26370  dchrelbas2  26394  dchreq  26415  dchrsum  26426  gausslemma2dlem4  26526  2sqreultblem  26605  dchrisum0fno1  26668  rplogsum  26684  islnopp  27109  frgrncvvdeq  28682  fusgr2wsp2nb  28707  eleigvec  30328  strlem1  30621  strlem5  30626  hstrlem5  30634  difrab2  30854  nfpconfp  30976  suppiniseg  31029  suppss3  31068  fsuppcurry1  31069  fsuppcurry2  31070  xrdifh  31110  nndiffz1  31116  ist0cld  31792  ordtconnlem1  31883  esumpinfval  32050  eulerpartlems  32336  eulerpartlemgc  32338  eulerpartlemb  32344  eulerpartlemf  32346  eulerpartlemt  32347  eulerpartlemgh  32354  ballotlemodife  32473  ballotth  32513  reprdifc  32616  hgt750lemb  32645  elmrsubrn  33491  mrsubvrs  33493  dftr6  33727  dffr5  33730  xpord2pred  33801  xpord2ind  33803  xpord3pred  33807  newbday  34091  sltlpss  34096  brsset  34200  dfon3  34203  ellimits  34221  dffun10  34225  elfuns  34226  fullfunfv  34258  dfrecs2  34261  dfrdg4  34262  dfint3  34263  hfext  34494  onsucsuccmpi  34641  bj-rest10b  35269  difunieq  35554  pibt2  35597  iundif1  35760  lindsadd  35779  poimirlem2  35788  poimirlem11  35797  poimirlem12  35798  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  poimirlem30  35816  itg2addnclem  35837  ftc1anclem5  35863  areacirc  35879  fdc  35912  isfldidl  36235  opelvvdif  36406  iswatN  38015  dochsnkrlem1  39490  selvval2lem5  40236  fsuppssindlem1  40287  ellz1  40596  pellexlem4  40661  pellexlem5  40662  infordmin  41146  minregex  41148  pwinfig  41175  elnonrel  41200  sqrtcvallem1  41246  clsk3nimkb  41657  ntrclselnel1  41674  ntrneiel2  41703  ntrneik4w  41717  undif3VD  42509  limcrecl  43177  icccncfext  43435  dvmptfprodlem  43492  stoweidlem26  43574  stoweidlem39  43587  stoweidlem52  43600  fourierdlem42  43697  etransclem18  43800  etransclem46  43828  ovolval4lem1  44194  requad01  45084  0ringdif  45439  0ring1eq0  45441  lindslinindsimp1  45809  dignn0fr  45958