Theorem eldif 3946

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 3512	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3512	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 483	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2900	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2900	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 320	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3939	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3668	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 382	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  Vcvv 3494   ∖ cdif 3933

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939

This theorem is referenced by:  eldifd  3947  eldifad  3948  eldifbd  3949  elneeldif  3950  velcomp  3951  difeqri  4101  eldifi  4103  eldifn  4104  neldif  4106  difdif  4107  ddif  4113  ssconb  4114  sscon  4115  ssdif  4116  raldifb  4121  elsymdif  4224  dfss4  4235  dfun2  4236  dfin2  4237  difin  4238  indifdir  4260  undif3  4265  difin2  4266  dfnul2OLD  4294  ssdif0  4323  difin0ss  4328  inssdif0  4329  reldisj  4402  disj3  4403  undif4  4416  pssnel  4420  inundif  4427  ssundif  4433  eldifpr  4597  elpwunsn  4621  eldiftp  4624  eldifsn  4719  eldifsnneqOLD  4724  difprsnss  4732  iundif2  4996  iindif1  4997  iindif2  4999  disjss3  5065  brdif  5119  difopab  5702  intirr  5978  cnvdif  6002  difxp  6021  xpdifid  6025  wfi  6181  ordunidif  6239  onmindif  6280  imadif  6438  dffv2  6756  eldifpw  7490  releldmdifi  7744  funeldmdif  7747  ressuppssdif  7851  extmptsuppeq  7854  suppss  7860  suppssr  7861  suppss2  7864  suppofssd  7867  ondif2  8127  oelim2  8221  boxcutc  8505  brsdom  8532  brsdom2  8641  php3  8703  unblem1  8770  unfilem1  8782  elfi2  8878  dfsup2  8908  ordtypelem7  8988  kmlem4  9579  ackbij1lem18  9659  infpssr  9730  isf34lem4  9799  fin17  9816  fin67  9817  dffin7-2  9820  fin1a2lem6  9827  axcclem  9879  pwfseqlem3  10082  grothprim  10256  xrlenlt  10706  nzadd  12031  irradd  12373  irrmul  12374  difreicc  12871  modirr  13311  hashinf  13696  sumss  15081  fsumss  15082  prodss  15301  fprodss  15302  fprodn0f  15345  rpnnen2lem12  15578  dvdsaddre2b  15657  sumeven  15738  bitscmp  15787  lcmfunsnlem2  15984  iserodd  16172  prmodvdslcmf  16383  symgfix2  18544  pmtrdifellem4  18607  sylow2alem2  18743  efgsfo  18865  gsumval3  19027  gsum2dlem1  19090  gsum2dlem2  19091  ablfac1eu  19195  gsumdixp  19359  isnirred  19450  isirred2  19451  irredn0  19453  lsppratlem1  19919  lbsextlem2  19931  mplsubrglem  20219  mplcoe1  20246  mplcoe5  20249  opsrtoslem2  20265  xrsmgmdifsgrp  20582  psgnodpm  20732  symgmatr01lem  21262  elcls  21681  isclo  21695  maxlp  21755  restntr  21790  isreg2  21985  cmpcld  22010  hausdiag  22253  txkgen  22260  kqcldsat  22341  ufinffr  22537  fin1aufil  22540  alexsublem  22652  alexsubALTlem3  22657  ptcmplem5  22664  blcld  23115  shftmbl  24139  vitalilem4  24212  vitalilem5  24213  vitali  24214  mbfeqalem1  24242  itg1val2  24285  itg10a  24311  itg1ge0a  24312  mbfi1fseqlem4  24319  itg2uba  24344  itg2splitlem  24349  itg2monolem1  24351  itg2cnlem1  24362  itg2cnlem2  24363  itgss  24412  dvtaylp  24958  pserdvlem2  25016  ellogdm  25222  relogbcxp  25363  cxplogb  25364  logbmpt  25366  atandm  25454  atans2  25509  eldmgm  25599  igamgam  25626  igamf  25628  igamcl  25629  lgam1  25641  gam1  25642  wilthlem2  25646  basellem3  25660  fsumvma  25789  dchrelbas2  25813  dchreq  25834  dchrsum  25845  gausslemma2dlem4  25945  2sqreultblem  26024  dchrisum0fno1  26087  rplogsum  26103  islnopp  26525  frgrncvvdeq  28088  fusgr2wsp2nb  28113  eleigvec  29734  strlem1  30027  strlem5  30032  hstrlem5  30040  difrab2  30261  nfpconfp  30377  suppss3  30460  fsuppcurry1  30461  fsuppcurry2  30462  xrdifh  30503  nndiffz1  30509  ordtconnlem1  31167  esumpinfval  31332  eulerpartlems  31618  eulerpartlemgc  31620  eulerpartlemb  31626  eulerpartlemf  31628  eulerpartlemt  31629  eulerpartlemgh  31636  ballotlemodife  31755  ballotth  31795  reprdifc  31898  hgt750lemb  31927  elmrsubrn  32767  mrsubvrs  32769  dftr6  32986  dffr5  32989  frpoind  33080  frind  33085  brsset  33350  dfon3  33353  ellimits  33371  dffun10  33375  elfuns  33376  fullfunfv  33408  dfrecs2  33411  dfrdg4  33412  dfint3  33413  hfext  33644  onsucsuccmpi  33791  bj-rest10b  34383  difunieq  34658  pibt2  34701  iundif1  34881  lindsadd  34900  poimirlem2  34909  poimirlem11  34918  poimirlem12  34919  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  poimirlem30  34937  itg2addnclem  34958  ftc1anclem5  34986  areacirc  35002  fdc  35035  isfldidl  35361  opelvvdif  35535  iswatN  37145  dochsnkrlem1  38620  selvval2lem5  39186  ellz1  39413  pellexlem4  39478  pellexlem5  39479  infordmin  39948  pwinfig  39969  elnonrel  39994  clsk3nimkb  40439  ntrclselnel1  40456  ntrneiel2  40485  ntrneik4w  40499  undif3VD  41265  limcrecl  41959  icccncfext  42219  dvmptfprodlem  42278  stoweidlem26  42360  stoweidlem39  42373  stoweidlem52  42386  fourierdlem42  42483  etransclem18  42586  etransclem46  42614  ovolval4lem1  42980  requad01  43835  0ringdif  44190  0ring1eq0  44192  lindslinindsimp1  44561  dignn0fr  44710