Theorem eldif 3911

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 3461	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3461	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2824	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2824	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 318	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3904	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3635	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ∖ cdif 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904

This theorem is referenced by:  eldifd  3912  eldifad  3913  eldifbd  3914  elneeldif  3915  velcomp  3916  difeqri  4080  nfdif  4081  eldifi  4083  eldifn  4084  neldif  4086  difdif  4087  ddif  4093  ssconb  4094  sscon  4095  ssdif  4096  raldifb  4101  elsymdif  4210  dfss4  4221  dfun2  4222  dfin2  4223  difin  4224  indifdi  4246  undif3  4252  difin2  4253  ssdif0  4318  difin0ss  4325  inssdif0  4326  reldisj  4405  disj3  4406  undif4  4419  pssnel  4423  inundif  4431  ssundif  4440  eldifpr  4615  elpwunsn  4641  eldiftp  4644  eldifsn  4742  difprsnss  4755  iundif2  5029  iindif1  5030  iindif2  5032  disjss3  5097  brdif  5151  dffr6  5580  difopab  5779  intirr  6075  cnvdif  6101  difxp  6122  xpdifid  6126  frpoind  6300  ordunidif  6367  onmindif  6411  imadif  6576  dffv2  6929  eldifpw  7713  releldmdifi  7989  funeldmdif  7992  xpord2pred  8087  xpord2indlem  8089  ressuppssdif  8127  extmptsuppeq  8130  suppss  8136  suppssr  8137  suppssrg  8138  suppss2  8142  suppofssd  8145  suppcoss  8149  ondif2  8429  oelim2  8523  eldifsucnn  8592  boxcutc  8879  brsdom  8911  brsdom2  9029  php3  9133  unblem1  9192  unfilem1  9205  elfi2  9317  dfsup2  9347  ordtypelem7  9429  ssttrcl  9624  ttrcltr  9625  dmttrcl  9630  frind  9662  kmlem4  10064  ackbij1lem18  10146  infpssr  10218  isf34lem4  10287  fin17  10304  fin67  10305  dffin7-2  10308  fin1a2lem6  10315  axcclem  10367  pwfseqlem3  10571  grothprim  10745  xrlenlt  11197  nzadd  12539  irradd  12886  irrmul  12887  difreicc  13400  fzdif1  13521  modirr  13865  hashinf  14258  sumss  15647  fsumss  15648  prodss  15870  fprodss  15871  fprodn0f  15914  rpnnen2lem12  16150  dvdsaddre2b  16234  sumeven  16314  bitscmp  16365  lcmfunsnlem2  16567  iserodd  16763  prmodvdslcmf  16975  chnccat  18549  symgfix2  19345  pmtrdifellem4  19408  sylow2alem2  19547  efgsfo  19668  gsumval3  19836  gsum2dlem1  19899  gsum2dlem2  19900  ablfac1eu  20004  gsumdixp  20254  isnirred  20356  isirred2  20357  irredn0  20359  0ringdif  20460  0ring1eq0  20466  lsppratlem1  21102  lbsextlem2  21114  xrsmgmdifsgrp  21363  psgnodpm  21543  mplsubrglem  21959  mplcoe1  21992  mplcoe5  21995  opsrtoslem2  22011  symgmatr01lem  22597  elcls  23017  isclo  23031  maxlp  23091  restntr  23126  isreg2  23321  cmpcld  23346  hausdiag  23589  txkgen  23596  kqcldsat  23677  ufinffr  23873  fin1aufil  23876  alexsublem  23988  alexsubALTlem3  23993  ptcmplem5  24000  blcld  24449  shftmbl  25495  vitalilem4  25568  vitalilem5  25569  vitali  25570  mbfeqalem1  25598  itg1val2  25641  itg10a  25667  itg1ge0a  25668  mbfi1fseqlem4  25675  itg2uba  25700  itg2splitlem  25705  itg2monolem1  25707  itg2cnlem1  25718  itg2cnlem2  25719  itgss  25769  dvtaylp  26334  pserdvlem2  26394  ellogdm  26604  relogbcxp  26751  cxplogb  26752  logbmpt  26754  atandm  26842  atans2  26897  eldmgm  26988  igamgam  27015  igamf  27017  igamcl  27018  lgam1  27030  gam1  27031  wilthlem2  27035  basellem3  27049  fsumvma  27180  dchrelbas2  27204  dchreq  27225  dchrsum  27236  gausslemma2dlem4  27336  2sqreultblem  27415  dchrisum0fno1  27478  rplogsum  27494  newbday  27898  ltslpss  27904  islnopp  28811  frgrncvvdeq  30384  fusgr2wsp2nb  30409  eleigvec  32032  strlem1  32325  strlem5  32330  hstrlem5  32338  difrab2  32572  nfpconfp  32710  fdifsupp  32764  suppiniseg  32765  suppss3  32802  fsuppcurry1  32803  fsuppcurry2  32804  xrdifh  32860  nndiffz1  32866  elrgspnsubrunlem2  33330  ist0cld  33990  ordtconnlem1  34081  esumpinfval  34230  eulerpartlems  34517  eulerpartlemgc  34519  eulerpartlemb  34525  eulerpartlemf  34527  eulerpartlemt  34528  eulerpartlemgh  34535  ballotlemodife  34655  ballotth  34695  reprdifc  34784  hgt750lemb  34813  onvf1od  35301  elmrsubrn  35714  mrsubvrs  35716  dftr6  35945  dffr5  35948  brsset  36081  dfon3  36084  ellimits  36102  dffun10  36106  elfuns  36107  fullfunfv  36141  dfrecs2  36144  dfrdg4  36145  dfint3  36146  hfext  36377  onsucsuccmpi  36637  bj-rest10b  37294  difunieq  37579  pibt2  37622  iundif1  37795  lindsadd  37814  poimirlem2  37823  poimirlem11  37832  poimirlem12  37833  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  poimirlem30  37851  itg2addnclem  37872  ftc1anclem5  37898  areacirc  37914  fdc  37946  isfldidl  38269  opelvvdif  38459  iswatN  40264  dochsnkrlem1  41739  unitscyglem4  42462  redvmptabs  42625  selvcllem5  42835  selvvvval  42838  fsuppssindlem1  42844  ellz1  43019  pellexlem4  43084  pellexlem5  43085  ordeldif  43510  ordeldifsucon  43511  ordeldif1o  43512  cantnfresb  43576  cantnf2  43577  oadif1lem  43631  oadif1  43632  infordmin  43783  minregex  43785  pwinfig  43812  elnonrel  43836  sqrtcvallem1  43882  clsk3nimkb  44291  ntrclselnel1  44308  ntrneiel2  44337  ntrneik4w  44351  undif3VD  45132  iindif2f  45414  limcrecl  45885  icccncfext  46141  dvmptfprodlem  46198  stoweidlem26  46280  stoweidlem39  46293  stoweidlem52  46306  fourierdlem42  46403  etransclem18  46506  etransclem46  46534  ovolval4lem1  46903  nthrucw  47140  requad01  47877  dfnbgr6  48113  lindslinindsimp1  48713  dignn0fr  48857