Theorem eldif 3959

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952

This theorem is referenced by:  eldifd  3960  eldifad  3961  eldifbd  3962  elneeldif  3963  velcomp  3964  difeqri  4125  eldifi  4127  eldifn  4128  neldif  4130  difdif  4131  ddif  4137  ssconb  4138  sscon  4139  ssdif  4140  raldifb  4145  elsymdif  4248  dfss4  4259  dfun2  4260  dfin2  4261  difin  4262  indifdi  4284  indifdirOLD  4286  undif3  4291  difin2  4292  ssdif0  4364  difin0ss  4369  inssdif0  4370  reldisj  4452  reldisjOLD  4453  disj3  4454  undif4  4467  pssnel  4471  inundif  4479  ssundif  4488  eldifpr  4661  elpwunsn  4688  eldiftp  4691  eldifsn  4791  difprsnss  4803  iundif2  5078  iindif1  5079  iindif2  5081  disjss3  5148  brdif  5202  dffr6  5635  difopab  5831  difopabOLD  5832  intirr  6120  cnvdif  6144  difxp  6164  xpdifid  6168  frpoind  6344  wfiOLD  6353  ordunidif  6414  onmindif  6457  imadif  6633  dffv2  6987  eldifpw  7755  releldmdifi  8031  funeldmdif  8034  xpord2pred  8131  xpord2indlem  8133  ressuppssdif  8170  extmptsuppeq  8173  suppss  8179  suppssOLD  8180  suppssr  8181  suppssrg  8182  suppss2  8185  suppofssd  8188  suppcoss  8192  ondif2  8502  oelim2  8595  eldifsucnn  8663  boxcutc  8935  brsdom  8971  brsdom2  9097  php3  9212  php3OLD  9224  unblem1  9295  unfilem1  9310  elfi2  9409  dfsup2  9439  ordtypelem7  9519  ssttrcl  9710  ttrcltr  9711  dmttrcl  9716  frind  9745  kmlem4  10148  ackbij1lem18  10232  infpssr  10303  isf34lem4  10372  fin17  10389  fin67  10390  dffin7-2  10393  fin1a2lem6  10400  axcclem  10452  pwfseqlem3  10655  grothprim  10829  xrlenlt  11279  nzadd  12610  irradd  12957  irrmul  12958  difreicc  13461  modirr  13907  hashinf  14295  sumss  15670  fsumss  15671  prodss  15891  fprodss  15892  fprodn0f  15935  rpnnen2lem12  16168  dvdsaddre2b  16250  sumeven  16330  bitscmp  16379  lcmfunsnlem2  16577  iserodd  16768  prmodvdslcmf  16980  symgfix2  19284  pmtrdifellem4  19347  sylow2alem2  19486  efgsfo  19607  gsumval3  19775  gsum2dlem1  19838  gsum2dlem2  19839  ablfac1eu  19943  gsumdixp  20131  isnirred  20234  isirred2  20235  irredn0  20237  lsppratlem1  20760  lbsextlem2  20772  xrsmgmdifsgrp  20982  psgnodpm  21141  mplsubrglem  21563  mplcoe1  21592  mplcoe5  21595  opsrtoslem2  21617  symgmatr01lem  22155  elcls  22577  isclo  22591  maxlp  22651  restntr  22686  isreg2  22881  cmpcld  22906  hausdiag  23149  txkgen  23156  kqcldsat  23237  ufinffr  23433  fin1aufil  23436  alexsublem  23548  alexsubALTlem3  23553  ptcmplem5  23560  blcld  24014  shftmbl  25055  vitalilem4  25128  vitalilem5  25129  vitali  25130  mbfeqalem1  25158  itg1val2  25201  itg10a  25228  itg1ge0a  25229  mbfi1fseqlem4  25236  itg2uba  25261  itg2splitlem  25266  itg2monolem1  25268  itg2cnlem1  25279  itg2cnlem2  25280  itgss  25329  dvtaylp  25882  pserdvlem2  25940  ellogdm  26147  relogbcxp  26290  cxplogb  26291  logbmpt  26293  atandm  26381  atans2  26436  eldmgm  26526  igamgam  26553  igamf  26555  igamcl  26556  lgam1  26568  gam1  26569  wilthlem2  26573  basellem3  26587  fsumvma  26716  dchrelbas2  26740  dchreq  26761  dchrsum  26772  gausslemma2dlem4  26872  2sqreultblem  26951  dchrisum0fno1  27014  rplogsum  27030  newbday  27396  sltlpss  27401  islnopp  27990  frgrncvvdeq  29562  fusgr2wsp2nb  29587  eleigvec  31210  strlem1  31503  strlem5  31508  hstrlem5  31516  difrab2  31738  nfpconfp  31856  suppiniseg  31908  suppss3  31949  fsuppcurry1  31950  fsuppcurry2  31951  xrdifh  31991  nndiffz1  31997  ist0cld  32813  ordtconnlem1  32904  esumpinfval  33071  eulerpartlems  33359  eulerpartlemgc  33361  eulerpartlemb  33367  eulerpartlemf  33369  eulerpartlemt  33370  eulerpartlemgh  33377  ballotlemodife  33496  ballotth  33536  reprdifc  33639  hgt750lemb  33668  elmrsubrn  34511  mrsubvrs  34513  dftr6  34721  dffr5  34724  brsset  34861  dfon3  34864  ellimits  34882  dffun10  34886  elfuns  34887  fullfunfv  34919  dfrecs2  34922  dfrdg4  34923  dfint3  34924  hfext  35155  onsucsuccmpi  35328  bj-rest10b  35970  difunieq  36255  pibt2  36298  iundif1  36462  lindsadd  36481  poimirlem2  36490  poimirlem11  36499  poimirlem12  36500  poimirlem18  36506  poimirlem21  36509  poimirlem22  36510  poimirlem30  36518  itg2addnclem  36539  ftc1anclem5  36565  areacirc  36581  fdc  36613  isfldidl  36936  opelvvdif  37127  iswatN  38865  dochsnkrlem1  40340  selvcllem5  41154  selvvvval  41157  fsuppssindlem1  41163  ellz1  41505  pellexlem4  41570  pellexlem5  41571  ordeldif  42008  ordeldifsucon  42009  ordeldif1o  42010  cantnfresb  42074  cantnf2  42075  oadif1lem  42129  oadif1  42130  infordmin  42283  minregex  42285  pwinfig  42312  elnonrel  42336  sqrtcvallem1  42382  clsk3nimkb  42791  ntrclselnel1  42808  ntrneiel2  42837  ntrneik4w  42851  undif3VD  43643  iindif2f  43854  limcrecl  44345  icccncfext  44603  dvmptfprodlem  44660  stoweidlem26  44742  stoweidlem39  44755  stoweidlem52  44768  fourierdlem42  44865  etransclem18  44968  etransclem46  44996  ovolval4lem1  45365  requad01  46289  0ringdif  46644  0ring1eq0  46646  lindslinindsimp1  47138  dignn0fr  47287