Theorem eldif 3972

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965

This theorem is referenced by:  eldifd  3973  eldifad  3974  eldifbd  3975  elneeldif  3976  velcomp  3977  difeqri  4137  nfdif  4138  eldifi  4140  eldifn  4141  neldif  4143  difdif  4144  ddif  4150  ssconb  4151  sscon  4152  ssdif  4153  raldifb  4158  elsymdif  4263  dfss4  4274  dfun2  4275  dfin2  4276  difin  4277  indifdi  4299  undif3  4305  difin2  4306  ssdif0  4371  difin0ss  4378  inssdif0  4379  reldisj  4458  disj3  4459  undif4  4472  pssnel  4476  inundif  4484  ssundif  4493  eldifpr  4662  elpwunsn  4688  eldiftp  4691  eldifsn  4790  difprsnss  4803  iundif2  5078  iindif1  5079  iindif2  5081  disjss3  5146  brdif  5200  dffr6  5643  difopab  5842  difopabOLD  5843  intirr  6140  cnvdif  6165  difxp  6185  xpdifid  6189  frpoind  6364  wfiOLD  6373  ordunidif  6434  onmindif  6477  imadif  6651  dffv2  7003  eldifpw  7786  releldmdifi  8068  funeldmdif  8071  xpord2pred  8168  xpord2indlem  8170  ressuppssdif  8208  extmptsuppeq  8211  suppss  8217  suppssr  8218  suppssrg  8219  suppss2  8223  suppofssd  8226  suppcoss  8230  ondif2  8538  oelim2  8631  eldifsucnn  8700  boxcutc  8979  brsdom  9013  brsdom2  9135  php3  9246  php3OLD  9258  unblem1  9325  unfilem1  9340  elfi2  9451  dfsup2  9481  ordtypelem7  9561  ssttrcl  9752  ttrcltr  9753  dmttrcl  9758  frind  9787  kmlem4  10191  ackbij1lem18  10273  infpssr  10345  isf34lem4  10414  fin17  10431  fin67  10432  dffin7-2  10435  fin1a2lem6  10442  axcclem  10494  pwfseqlem3  10697  grothprim  10871  xrlenlt  11323  nzadd  12662  irradd  13012  irrmul  13013  difreicc  13520  fzdif1  13641  modirr  13979  hashinf  14370  sumss  15756  fsumss  15757  prodss  15979  fprodss  15980  fprodn0f  16023  rpnnen2lem12  16257  dvdsaddre2b  16340  sumeven  16420  bitscmp  16471  lcmfunsnlem2  16673  iserodd  16868  prmodvdslcmf  17080  symgfix2  19448  pmtrdifellem4  19511  sylow2alem2  19650  efgsfo  19771  gsumval3  19939  gsum2dlem1  20002  gsum2dlem2  20003  ablfac1eu  20107  gsumdixp  20332  isnirred  20436  isirred2  20437  irredn0  20439  0ringdif  20543  0ring1eq0  20549  lsppratlem1  21166  lbsextlem2  21178  xrsmgmdifsgrp  21438  psgnodpm  21623  mplsubrglem  22041  mplcoe1  22072  mplcoe5  22075  opsrtoslem2  22097  symgmatr01lem  22674  elcls  23096  isclo  23110  maxlp  23170  restntr  23205  isreg2  23400  cmpcld  23425  hausdiag  23668  txkgen  23675  kqcldsat  23756  ufinffr  23952  fin1aufil  23955  alexsublem  24067  alexsubALTlem3  24072  ptcmplem5  24079  blcld  24533  shftmbl  25586  vitalilem4  25659  vitalilem5  25660  vitali  25661  mbfeqalem1  25689  itg1val2  25732  itg10a  25759  itg1ge0a  25760  mbfi1fseqlem4  25767  itg2uba  25792  itg2splitlem  25797  itg2monolem1  25799  itg2cnlem1  25810  itg2cnlem2  25811  itgss  25861  dvtaylp  26426  pserdvlem2  26486  ellogdm  26695  relogbcxp  26842  cxplogb  26843  logbmpt  26845  atandm  26933  atans2  26988  eldmgm  27079  igamgam  27106  igamf  27108  igamcl  27109  lgam1  27121  gam1  27122  wilthlem2  27126  basellem3  27140  fsumvma  27271  dchrelbas2  27295  dchreq  27316  dchrsum  27327  gausslemma2dlem4  27427  2sqreultblem  27506  dchrisum0fno1  27569  rplogsum  27585  newbday  27954  sltlpss  27959  islnopp  28761  frgrncvvdeq  30337  fusgr2wsp2nb  30362  eleigvec  31985  strlem1  32278  strlem5  32283  hstrlem5  32291  difrab2  32525  nfpconfp  32648  fdifsupp  32699  suppiniseg  32700  suppss3  32741  fsuppcurry1  32742  fsuppcurry2  32743  xrdifh  32788  nndiffz1  32794  ist0cld  33793  ordtconnlem1  33884  esumpinfval  34053  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemb  34349  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartlemgh  34359  ballotlemodife  34478  ballotth  34518  reprdifc  34620  hgt750lemb  34649  elmrsubrn  35504  mrsubvrs  35506  dftr6  35730  dffr5  35733  brsset  35870  dfon3  35873  ellimits  35891  dffun10  35895  elfuns  35896  fullfunfv  35928  dfrecs2  35931  dfrdg4  35932  dfint3  35933  hfext  36164  onsucsuccmpi  36425  bj-rest10b  37071  difunieq  37356  pibt2  37399  iundif1  37580  lindsadd  37599  poimirlem2  37608  poimirlem11  37617  poimirlem12  37618  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem30  37636  itg2addnclem  37657  ftc1anclem5  37683  areacirc  37699  fdc  37731  isfldidl  38054  opelvvdif  38240  iswatN  39976  dochsnkrlem1  41451  unitscyglem4  42179  redvmptabs  42368  selvcllem5  42568  selvvvval  42571  fsuppssindlem1  42577  ellz1  42754  pellexlem4  42819  pellexlem5  42820  ordeldif  43247  ordeldifsucon  43248  ordeldif1o  43249  cantnfresb  43313  cantnf2  43314  oadif1lem  43368  oadif1  43369  infordmin  43521  minregex  43523  pwinfig  43550  elnonrel  43574  sqrtcvallem1  43620  clsk3nimkb  44029  ntrclselnel1  44046  ntrneiel2  44075  ntrneik4w  44089  undif3VD  44879  iindif2f  45102  limcrecl  45584  icccncfext  45842  dvmptfprodlem  45899  stoweidlem26  45981  stoweidlem39  45994  stoweidlem52  46007  fourierdlem42  46104  etransclem18  46207  etransclem46  46235  ovolval4lem1  46604  requad01  47545  dfnbgr6  47780  lindslinindsimp1  48302  dignn0fr  48450