Theorem eldif 3909

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902

This theorem is referenced by:  eldifd  3910  eldifad  3911  eldifbd  3912  elneeldif  3913  velcomp  3914  difeqri  4078  nfdif  4079  eldifi  4081  eldifn  4082  neldif  4084  difdif  4085  ddif  4091  ssconb  4092  sscon  4093  ssdif  4094  raldifb  4099  elsymdif  4208  dfss4  4219  dfun2  4220  dfin2  4221  difin  4222  indifdi  4244  undif3  4250  difin2  4251  ssdif0  4316  difin0ss  4323  inssdif0  4324  reldisj  4403  disj3  4404  undif4  4417  pssnel  4421  inundif  4429  ssundif  4438  eldifpr  4613  elpwunsn  4639  eldiftp  4642  eldifsn  4740  difprsnss  4753  iundif2  5027  iindif1  5028  iindif2  5030  disjss3  5095  brdif  5149  dffr6  5578  difopab  5777  intirr  6073  cnvdif  6099  difxp  6120  xpdifid  6124  frpoind  6298  ordunidif  6365  onmindif  6409  imadif  6574  dffv2  6927  eldifpw  7711  releldmdifi  7987  funeldmdif  7990  xpord2pred  8085  xpord2indlem  8087  ressuppssdif  8125  extmptsuppeq  8128  suppss  8134  suppssr  8135  suppssrg  8136  suppss2  8140  suppofssd  8143  suppcoss  8147  ondif2  8427  oelim2  8521  eldifsucnn  8590  boxcutc  8877  brsdom  8909  brsdom2  9027  php3  9131  unblem1  9190  unfilem1  9203  elfi2  9315  dfsup2  9345  ordtypelem7  9427  ssttrcl  9622  ttrcltr  9623  dmttrcl  9628  frind  9660  kmlem4  10062  ackbij1lem18  10144  infpssr  10216  isf34lem4  10285  fin17  10302  fin67  10303  dffin7-2  10306  fin1a2lem6  10313  axcclem  10365  pwfseqlem3  10569  grothprim  10743  xrlenlt  11195  nzadd  12537  irradd  12884  irrmul  12885  difreicc  13398  fzdif1  13519  modirr  13863  hashinf  14256  sumss  15645  fsumss  15646  prodss  15868  fprodss  15869  fprodn0f  15912  rpnnen2lem12  16148  dvdsaddre2b  16232  sumeven  16312  bitscmp  16363  lcmfunsnlem2  16565  iserodd  16761  prmodvdslcmf  16973  chnccat  18547  symgfix2  19343  pmtrdifellem4  19406  sylow2alem2  19545  efgsfo  19666  gsumval3  19834  gsum2dlem1  19897  gsum2dlem2  19898  ablfac1eu  20002  gsumdixp  20252  isnirred  20354  isirred2  20355  irredn0  20357  0ringdif  20458  0ring1eq0  20464  lsppratlem1  21100  lbsextlem2  21112  xrsmgmdifsgrp  21361  psgnodpm  21541  mplsubrglem  21957  mplcoe1  21990  mplcoe5  21993  opsrtoslem2  22009  symgmatr01lem  22595  elcls  23015  isclo  23029  maxlp  23089  restntr  23124  isreg2  23319  cmpcld  23344  hausdiag  23587  txkgen  23594  kqcldsat  23675  ufinffr  23871  fin1aufil  23874  alexsublem  23986  alexsubALTlem3  23991  ptcmplem5  23998  blcld  24447  shftmbl  25493  vitalilem4  25566  vitalilem5  25567  vitali  25568  mbfeqalem1  25596  itg1val2  25639  itg10a  25665  itg1ge0a  25666  mbfi1fseqlem4  25673  itg2uba  25698  itg2splitlem  25703  itg2monolem1  25705  itg2cnlem1  25716  itg2cnlem2  25717  itgss  25767  dvtaylp  26332  pserdvlem2  26392  ellogdm  26602  relogbcxp  26749  cxplogb  26750  logbmpt  26752  atandm  26840  atans2  26895  eldmgm  26986  igamgam  27013  igamf  27015  igamcl  27016  lgam1  27028  gam1  27029  wilthlem2  27033  basellem3  27047  fsumvma  27178  dchrelbas2  27202  dchreq  27223  dchrsum  27234  gausslemma2dlem4  27334  2sqreultblem  27413  dchrisum0fno1  27476  rplogsum  27492  newbday  27874  sltlpss  27880  islnopp  28760  frgrncvvdeq  30333  fusgr2wsp2nb  30358  eleigvec  31981  strlem1  32274  strlem5  32279  hstrlem5  32287  difrab2  32521  nfpconfp  32659  fdifsupp  32713  suppiniseg  32714  suppss3  32751  fsuppcurry1  32752  fsuppcurry2  32753  xrdifh  32809  nndiffz1  32815  elrgspnsubrunlem2  33279  ist0cld  33939  ordtconnlem1  34030  esumpinfval  34179  eulerpartlems  34466  eulerpartlemgc  34468  eulerpartlemb  34474  eulerpartlemf  34476  eulerpartlemt  34477  eulerpartlemgh  34484  ballotlemodife  34604  ballotth  34644  reprdifc  34733  hgt750lemb  34762  onvf1od  35250  elmrsubrn  35663  mrsubvrs  35665  dftr6  35894  dffr5  35897  brsset  36030  dfon3  36033  ellimits  36051  dffun10  36055  elfuns  36056  fullfunfv  36090  dfrecs2  36093  dfrdg4  36094  dfint3  36095  hfext  36326  onsucsuccmpi  36586  bj-rest10b  37233  difunieq  37518  pibt2  37561  iundif1  37734  lindsadd  37753  poimirlem2  37762  poimirlem11  37771  poimirlem12  37772  poimirlem18  37778  poimirlem21  37781  poimirlem22  37782  poimirlem30  37790  itg2addnclem  37811  ftc1anclem5  37837  areacirc  37853  fdc  37885  isfldidl  38208  opelvvdif  38396  iswatN  40193  dochsnkrlem1  41668  unitscyglem4  42391  redvmptabs  42557  selvcllem5  42767  selvvvval  42770  fsuppssindlem1  42776  ellz1  42951  pellexlem4  43016  pellexlem5  43017  ordeldif  43442  ordeldifsucon  43443  ordeldif1o  43444  cantnfresb  43508  cantnf2  43509  oadif1lem  43563  oadif1  43564  infordmin  43715  minregex  43717  pwinfig  43744  elnonrel  43768  sqrtcvallem1  43814  clsk3nimkb  44223  ntrclselnel1  44240  ntrneiel2  44269  ntrneik4w  44283  undif3VD  45064  iindif2f  45346  limcrecl  45817  icccncfext  46073  dvmptfprodlem  46130  stoweidlem26  46212  stoweidlem39  46225  stoweidlem52  46238  fourierdlem42  46335  etransclem18  46438  etransclem46  46466  ovolval4lem1  46835  nthrucw  47072  requad01  47809  dfnbgr6  48045  lindslinindsimp1  48645  dignn0fr  48789