Theorem eldif 3936

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 3480	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3480	. . 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 3929	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3659	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ∖ cdif 3923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929

This theorem is referenced by:  eldifd  3937  eldifad  3938  eldifbd  3939  elneeldif  3940  velcomp  3941  difeqri  4103  nfdif  4104  eldifi  4106  eldifn  4107  neldif  4109  difdif  4110  ddif  4116  ssconb  4117  sscon  4118  ssdif  4119  raldifb  4124  elsymdif  4233  dfss4  4244  dfun2  4245  dfin2  4246  difin  4247  indifdi  4269  undif3  4275  difin2  4276  ssdif0  4341  difin0ss  4348  inssdif0  4349  reldisj  4428  disj3  4429  undif4  4442  pssnel  4446  inundif  4454  ssundif  4463  eldifpr  4634  elpwunsn  4660  eldiftp  4663  eldifsn  4762  difprsnss  4775  iundif2  5050  iindif1  5051  iindif2  5053  disjss3  5118  brdif  5172  dffr6  5609  difopab  5809  difopabOLD  5810  intirr  6107  cnvdif  6132  difxp  6153  xpdifid  6157  frpoind  6331  wfiOLD  6340  ordunidif  6402  onmindif  6445  imadif  6619  dffv2  6973  eldifpw  7760  releldmdifi  8042  funeldmdif  8045  xpord2pred  8142  xpord2indlem  8144  ressuppssdif  8182  extmptsuppeq  8185  suppss  8191  suppssr  8192  suppssrg  8193  suppss2  8197  suppofssd  8200  suppcoss  8204  ondif2  8512  oelim2  8605  eldifsucnn  8674  boxcutc  8953  brsdom  8987  brsdom2  9109  php3  9221  php3OLD  9231  unblem1  9298  unfilem1  9313  elfi2  9424  dfsup2  9454  ordtypelem7  9536  ssttrcl  9727  ttrcltr  9728  dmttrcl  9733  frind  9762  kmlem4  10166  ackbij1lem18  10248  infpssr  10320  isf34lem4  10389  fin17  10406  fin67  10407  dffin7-2  10410  fin1a2lem6  10417  axcclem  10469  pwfseqlem3  10672  grothprim  10846  xrlenlt  11298  nzadd  12638  irradd  12987  irrmul  12988  difreicc  13499  fzdif1  13620  modirr  13958  hashinf  14351  sumss  15738  fsumss  15739  prodss  15961  fprodss  15962  fprodn0f  16005  rpnnen2lem12  16241  dvdsaddre2b  16324  sumeven  16404  bitscmp  16455  lcmfunsnlem2  16657  iserodd  16853  prmodvdslcmf  17065  symgfix2  19395  pmtrdifellem4  19458  sylow2alem2  19597  efgsfo  19718  gsumval3  19886  gsum2dlem1  19949  gsum2dlem2  19950  ablfac1eu  20054  gsumdixp  20277  isnirred  20378  isirred2  20379  irredn0  20381  0ringdif  20485  0ring1eq0  20491  lsppratlem1  21106  lbsextlem2  21118  xrsmgmdifsgrp  21369  psgnodpm  21546  mplsubrglem  21962  mplcoe1  21993  mplcoe5  21996  opsrtoslem2  22012  symgmatr01lem  22589  elcls  23009  isclo  23023  maxlp  23083  restntr  23118  isreg2  23313  cmpcld  23338  hausdiag  23581  txkgen  23588  kqcldsat  23669  ufinffr  23865  fin1aufil  23868  alexsublem  23980  alexsubALTlem3  23985  ptcmplem5  23992  blcld  24442  shftmbl  25489  vitalilem4  25562  vitalilem5  25563  vitali  25564  mbfeqalem1  25592  itg1val2  25635  itg10a  25661  itg1ge0a  25662  mbfi1fseqlem4  25669  itg2uba  25694  itg2splitlem  25699  itg2monolem1  25701  itg2cnlem1  25712  itg2cnlem2  25713  itgss  25763  dvtaylp  26328  pserdvlem2  26388  ellogdm  26598  relogbcxp  26745  cxplogb  26746  logbmpt  26748  atandm  26836  atans2  26891  eldmgm  26982  igamgam  27009  igamf  27011  igamcl  27012  lgam1  27024  gam1  27025  wilthlem2  27029  basellem3  27043  fsumvma  27174  dchrelbas2  27198  dchreq  27219  dchrsum  27230  gausslemma2dlem4  27330  2sqreultblem  27409  dchrisum0fno1  27472  rplogsum  27488  newbday  27857  sltlpss  27862  islnopp  28664  frgrncvvdeq  30236  fusgr2wsp2nb  30261  eleigvec  31884  strlem1  32177  strlem5  32182  hstrlem5  32190  difrab2  32425  nfpconfp  32556  fdifsupp  32608  suppiniseg  32609  suppss3  32647  fsuppcurry1  32648  fsuppcurry2  32649  xrdifh  32703  nndiffz1  32709  elrgspnsubrunlem2  33189  ist0cld  33810  ordtconnlem1  33901  esumpinfval  34050  eulerpartlems  34338  eulerpartlemgc  34340  eulerpartlemb  34346  eulerpartlemf  34348  eulerpartlemt  34349  eulerpartlemgh  34356  ballotlemodife  34476  ballotth  34516  reprdifc  34605  hgt750lemb  34634  elmrsubrn  35488  mrsubvrs  35490  dftr6  35714  dffr5  35717  brsset  35853  dfon3  35856  ellimits  35874  dffun10  35878  elfuns  35879  fullfunfv  35911  dfrecs2  35914  dfrdg4  35915  dfint3  35916  hfext  36147  onsucsuccmpi  36407  bj-rest10b  37053  difunieq  37338  pibt2  37381  iundif1  37564  lindsadd  37583  poimirlem2  37592  poimirlem11  37601  poimirlem12  37602  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  poimirlem30  37620  itg2addnclem  37641  ftc1anclem5  37667  areacirc  37683  fdc  37715  isfldidl  38038  opelvvdif  38223  iswatN  39959  dochsnkrlem1  41434  unitscyglem4  42157  redvmptabs  42350  selvcllem5  42552  selvvvval  42555  fsuppssindlem1  42561  ellz1  42737  pellexlem4  42802  pellexlem5  42803  ordeldif  43229  ordeldifsucon  43230  ordeldif1o  43231  cantnfresb  43295  cantnf2  43296  oadif1lem  43350  oadif1  43351  infordmin  43503  minregex  43505  pwinfig  43532  elnonrel  43556  sqrtcvallem1  43602  clsk3nimkb  44011  ntrclselnel1  44028  ntrneiel2  44057  ntrneik4w  44071  undif3VD  44854  iindif2f  45132  limcrecl  45606  icccncfext  45864  dvmptfprodlem  45921  stoweidlem26  46003  stoweidlem39  46016  stoweidlem52  46029  fourierdlem42  46126  etransclem18  46229  etransclem46  46257  ovolval4lem1  46626  requad01  47583  dfnbgr6  47818  lindslinindsimp1  48381  dignn0fr  48529