Theorem eldif 3841

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 3433	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 3433	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 473	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2853	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2853	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 310	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 621	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3834	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3584	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 371	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050  Vcvv 3415   ∖ cdif 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-dif 3834

This theorem is referenced by:  eldifd  3842  eldifad  3843  eldifbd  3844  difeqri  3993  eldifi  3995  eldifn  3996  neldif  3998  difdif  3999  ddif  4005  ssconb  4006  sscon  4007  ssdif  4008  raldifb  4013  elsymdif  4113  dfss4  4124  dfun2  4125  dfin2  4126  difin  4127  indifdir  4149  undif3  4154  difin2  4155  dfnul2OLD  4183  ssdif0  4211  difin0ss  4216  inssdif0  4217  reldisj  4286  disj3  4287  undif4  4300  pssnel  4304  inundif  4311  ssundif  4317  eldifpr  4470  elpwunsn  4496  eldiftp  4499  eldifsn  4594  eldifsnneqOLD  4599  difprsnss  4607  iundif2  4863  iindif1  4864  iindif2  4866  disjss3  4929  brdif  4983  difopab  5553  intirr  5820  cnvdif  5844  difxp  5863  xpdifid  5867  wfi  6021  ordunidif  6079  onmindif  6120  imadif  6273  dffv2  6586  eldifpw  7309  ressuppssdif  7656  extmptsuppeq  7659  suppss  7665  suppssr  7666  suppss2  7669  suppofssd  7672  ondif2  7931  oelim2  8024  boxcutc  8304  brsdom  8331  brsdom2  8439  php3  8501  unblem1  8567  unfilem1  8579  elfi2  8675  dfsup2  8705  ordtypelem7  8785  kmlem4  9375  ackbij1lem18  9459  infpssr  9530  isf34lem4  9599  fin17  9616  fin67  9617  dffin7-2  9620  fin1a2lem6  9627  axcclem  9679  pwfseqlem3  9882  grothprim  10056  xrlenlt  10508  nzadd  11846  irradd  12190  irrmul  12191  difreicc  12689  modirr  13128  hashinf  13513  sumss  14944  fsumss  14945  prodss  15164  fprodss  15165  fprodn0f  15208  rpnnen2lem12  15441  dvdsaddre2b  15520  sumeven  15601  bitscmp  15650  lcmfunsnlem2  15843  iserodd  16031  prmodvdslcmf  16242  symgfix2  18308  pmtrdifellem4  18371  sylow2alem2  18507  efgsfo  18627  gsumval3  18784  gsum2dlem1  18846  gsum2dlem2  18847  ablfac1eu  18948  gsumdixp  19085  isnirred  19176  isirred2  19177  irredn0  19179  lsppratlem1  19644  lbsextlem2  19656  mplsubrglem  19936  mplcoe1  19962  mplcoe5  19965  opsrtoslem2  19981  xrsmgmdifsgrp  20287  psgnodpm  20437  symgmatr01lem  20969  elcls  21388  isclo  21402  maxlp  21462  restntr  21497  isreg2  21692  cmpcld  21717  hausdiag  21960  txkgen  21967  kqcldsat  22048  ufinffr  22244  fin1aufil  22247  alexsublem  22359  alexsubALTlem3  22364  ptcmplem5  22371  blcld  22821  shftmbl  23845  vitalilem4  23918  vitalilem5  23919  vitali  23920  mbfeqalem1  23948  itg1val2  23991  itg10a  24017  itg1ge0a  24018  mbfi1fseqlem4  24025  itg2uba  24050  itg2splitlem  24055  itg2monolem1  24057  itg2cnlem1  24068  itg2cnlem2  24069  itgss  24118  dvtaylp  24664  pserdvlem2  24722  ellogdm  24926  relogbcxp  25067  cxplogb  25068  logbmpt  25070  atandm  25158  atans2  25213  eldmgm  25304  igamgam  25331  igamf  25333  igamcl  25334  lgam1  25346  gam1  25347  wilthlem2  25351  basellem3  25365  fsumvma  25494  dchrelbas2  25518  dchreq  25539  dchrsum  25550  gausslemma2dlem4  25650  2sqreultblem  25729  dchrisum0fno1  25792  rplogsum  25808  islnopp  26230  frgrncvvdeq  27846  fusgr2wsp2nb  27871  eleigvec  29518  strlem1  29811  strlem5  29816  hstrlem5  29824  difrab2  30043  suppss3  30215  fsuppcurry1  30216  fsuppcurry2  30217  xrdifh  30258  nndiffz1  30264  ordtconnlem1  30811  esumpinfval  30976  eulerpartlems  31263  eulerpartlemgc  31265  eulerpartlemb  31271  eulerpartlemf  31273  eulerpartlemt  31274  eulerpartlemgh  31281  ballotlemodife  31401  ballotth  31441  reprdifc  31546  hgt750lemb  31575  elmrsubrn  32287  mrsubvrs  32289  dftr6  32506  dffr5  32509  frpoind  32601  frind  32606  brsset  32871  dfon3  32874  ellimits  32892  dffun10  32896  elfuns  32897  fullfunfv  32929  dfrecs2  32932  dfrdg4  32933  dfint3  32934  hfext  33165  onsucsuccmpi  33311  bj-rest10b  33890  difunieq  34097  pibt2  34139  iundif1  34307  lindsadd  34326  poimirlem2  34335  poimirlem11  34344  poimirlem12  34345  poimirlem18  34351  poimirlem21  34354  poimirlem22  34355  poimirlem30  34363  itg2addnclem  34384  ftc1anclem5  34412  areacirc  34428  fdc  34462  isfldidl  34788  opelvvdif  34964  iswatN  36575  dochsnkrlem1  38050  ellz1  38759  pellexlem4  38825  pellexlem5  38826  pwinfig  39282  elnonrel  39307  clsk3nimkb  39753  ntrclselnel1  39770  ntrneiel2  39799  ntrneik4w  39813  compel  40189  undif3VD  40635  limcrecl  41342  icccncfext  41601  dvmptfprodlem  41660  stoweidlem26  41743  stoweidlem39  41756  stoweidlem52  41769  fourierdlem42  41866  etransclem18  41969  etransclem46  41997  ovolval4lem1  42363  requad01  43155  0ringdif  43506  0ring1eq0  43508  lindslinindsimp1  43880  dignn0fr  44030