Theorem eldif 3893

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886

This theorem is referenced by:  eldifd  3894  eldifad  3895  eldifbd  3896  elneeldif  3897  velcomp  3898  difeqri  4055  eldifi  4057  eldifn  4058  neldif  4060  difdif  4061  ddif  4067  ssconb  4068  sscon  4069  ssdif  4070  raldifb  4075  elsymdif  4178  dfss4  4189  dfun2  4190  dfin2  4191  difin  4192  indifdi  4214  indifdirOLD  4216  undif3  4221  difin2  4222  ssdif0  4294  difin0ss  4299  inssdif0  4300  reldisj  4382  reldisjOLD  4383  disj3  4384  undif4  4397  pssnel  4401  inundif  4409  ssundif  4415  eldifpr  4590  elpwunsn  4616  eldiftp  4619  eldifsn  4717  difprsnss  4729  iundif2  4999  iindif1  5000  iindif2  5002  disjss3  5069  brdif  5123  dffr6  5538  difopab  5729  intirr  6012  cnvdif  6036  difxp  6056  xpdifid  6060  frpoind  6230  wfiOLD  6239  ordunidif  6299  onmindif  6340  imadif  6502  dffv2  6845  eldifpw  7596  releldmdifi  7859  funeldmdif  7862  ressuppssdif  7972  extmptsuppeq  7975  suppss  7981  suppssOLD  7982  suppssr  7983  suppssrg  7984  suppss2  7987  suppofssd  7990  suppcoss  7994  ondif2  8294  oelim2  8388  boxcutc  8687  brsdom  8718  brsdom2  8837  php3  8899  unblem1  8996  unfilem1  9008  elfi2  9103  dfsup2  9133  ordtypelem7  9213  frind  9439  kmlem4  9840  ackbij1lem18  9924  infpssr  9995  isf34lem4  10064  fin17  10081  fin67  10082  dffin7-2  10085  fin1a2lem6  10092  axcclem  10144  pwfseqlem3  10347  grothprim  10521  xrlenlt  10971  nzadd  12298  irradd  12642  irrmul  12643  difreicc  13145  modirr  13590  hashinf  13977  sumss  15364  fsumss  15365  prodss  15585  fprodss  15586  fprodn0f  15629  rpnnen2lem12  15862  dvdsaddre2b  15944  sumeven  16024  bitscmp  16073  lcmfunsnlem2  16273  iserodd  16464  prmodvdslcmf  16676  symgfix2  18939  pmtrdifellem4  19002  sylow2alem2  19138  efgsfo  19260  gsumval3  19423  gsum2dlem1  19486  gsum2dlem2  19487  ablfac1eu  19591  gsumdixp  19763  isnirred  19857  isirred2  19858  irredn0  19860  lsppratlem1  20324  lbsextlem2  20336  xrsmgmdifsgrp  20547  psgnodpm  20705  mplsubrglem  21120  mplcoe1  21148  mplcoe5  21151  opsrtoslem2  21173  symgmatr01lem  21710  elcls  22132  isclo  22146  maxlp  22206  restntr  22241  isreg2  22436  cmpcld  22461  hausdiag  22704  txkgen  22711  kqcldsat  22792  ufinffr  22988  fin1aufil  22991  alexsublem  23103  alexsubALTlem3  23108  ptcmplem5  23115  blcld  23567  shftmbl  24607  vitalilem4  24680  vitalilem5  24681  vitali  24682  mbfeqalem1  24710  itg1val2  24753  itg10a  24780  itg1ge0a  24781  mbfi1fseqlem4  24788  itg2uba  24813  itg2splitlem  24818  itg2monolem1  24820  itg2cnlem1  24831  itg2cnlem2  24832  itgss  24881  dvtaylp  25434  pserdvlem2  25492  ellogdm  25699  relogbcxp  25840  cxplogb  25841  logbmpt  25843  atandm  25931  atans2  25986  eldmgm  26076  igamgam  26103  igamf  26105  igamcl  26106  lgam1  26118  gam1  26119  wilthlem2  26123  basellem3  26137  fsumvma  26266  dchrelbas2  26290  dchreq  26311  dchrsum  26322  gausslemma2dlem4  26422  2sqreultblem  26501  dchrisum0fno1  26564  rplogsum  26580  islnopp  27004  frgrncvvdeq  28574  fusgr2wsp2nb  28599  eleigvec  30220  strlem1  30513  strlem5  30518  hstrlem5  30526  difrab2  30746  nfpconfp  30868  suppiniseg  30922  suppss3  30961  fsuppcurry1  30962  fsuppcurry2  30963  xrdifh  31003  nndiffz1  31009  ist0cld  31685  ordtconnlem1  31776  esumpinfval  31941  eulerpartlems  32227  eulerpartlemgc  32229  eulerpartlemb  32235  eulerpartlemf  32237  eulerpartlemt  32238  eulerpartlemgh  32245  ballotlemodife  32364  ballotth  32404  reprdifc  32507  hgt750lemb  32536  elmrsubrn  33382  mrsubvrs  33384  eldifsucnn  33597  dftr6  33624  dffr5  33627  ssttrcl  33701  ttrcltr  33702  dmttrcl  33707  xpord2pred  33719  xpord2ind  33721  xpord3pred  33725  newbday  34009  sltlpss  34014  brsset  34118  dfon3  34121  ellimits  34139  dffun10  34143  elfuns  34144  fullfunfv  34176  dfrecs2  34179  dfrdg4  34180  dfint3  34181  hfext  34412  onsucsuccmpi  34559  bj-rest10b  35187  difunieq  35472  pibt2  35515  iundif1  35678  lindsadd  35697  poimirlem2  35706  poimirlem11  35715  poimirlem12  35716  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem30  35734  itg2addnclem  35755  ftc1anclem5  35781  areacirc  35797  fdc  35830  isfldidl  36153  opelvvdif  36325  iswatN  37935  dochsnkrlem1  39410  selvval2lem5  40155  fsuppssindlem1  40203  ellz1  40505  pellexlem4  40570  pellexlem5  40571  infordmin  41037  pwinfig  41057  elnonrel  41082  sqrtcvallem1  41128  clsk3nimkb  41539  ntrclselnel1  41556  ntrneiel2  41585  ntrneik4w  41599  undif3VD  42391  limcrecl  43060  icccncfext  43318  dvmptfprodlem  43375  stoweidlem26  43457  stoweidlem39  43470  stoweidlem52  43483  fourierdlem42  43580  etransclem18  43683  etransclem46  43711  ovolval4lem1  44077  requad01  44961  0ringdif  45316  0ring1eq0  45318  lindslinindsimp1  45686  dignn0fr  45835