Theorem eldifd 3924

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3923. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
eldifd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eldifd.2	⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Assertion

Ref	Expression
eldifd	⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))

Proof of Theorem eldifd

Step	Hyp	Ref	Expression
1		eldifd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eldifd.2	. 2 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)
3		eldif 3923	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	1, 2, 3	sylanbrc 594	1 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916

This theorem is referenced by:  rexdifi  4112  eqoreldif  4656  frd  5619  xpdifid  6166  xpdifcnvepel  6167  funeldmdif  8045  ressuppssdif  8181  oaf1o  8548  findcard2d  9151  cantnflem1  9658  cantnflem2  9659  ttrcltr  9685  fin23lem26  10309  isf34lem4  10361  isfin7-2  10380  axdc3lem4  10437  axdc4lem  10439  ttukeylem7  10499  pwfseqlem1  10643  pwfseqlem3  10645  hashf1lem1  14492  seqcoll  14501  seqcoll2  14502  rlimcld2  15629  sumrblem  15762  fsumcvg  15763  fsumss  15776  incexclem  15890  prodrblem  15983  fprodcvg  15984  fprodss  16002  fprodn0f  16045  ruclem12  16297  sqrt2irr0  16307  coprmproddvdslem  16720  nnoddn2prmb  16873  prmreclem5  16980  ramub1lem1  17086  mreexd  17698  chnccats1  18681  chnccat  18682  frgpnabllem1  19943  gsumzaddlem  19991  gsum2d  20042  gsumxp2  20050  dmdprdsplitlem  20109  pgpfac1lem2  20147  pgpfac1lem3  20149  irredrmul  20509  lsppratlem3  21251  lbsextlem4  21263  prmidlsubm  21456  psgnodpmr  21709  frlmsslsp  21915  regsep2  23502  1stckgen  23680  regr1lem  23865  opnsubg  24234  zcld  24940  recld2  24941  bcthlem4  25455  iundisj  25676  iblss2  25934  itgeqa  25942  limcnlp  26006  plymulidp  26412  dvloglem  26779  dvlog2lem  26783  2irrexpq  26862  rtprmirr  26891  logbgcd1irr  26925  ressatans  27065  regamcl  27191  facgam  27196  wilthlem2  27199  2lgslem2  27525  noetasuplem4  27866  noetainflem4  27870  mulsval  28268  tgelrnln  28865  tglnpt4  28890  tgelrnpln  29016  lnincplng  29024  plngcplem  29025  plngrotlem1  29027  plngrotlem2  29028  lnssplnglem  29031  lnssplng  29032  nhpmirhp  29038  perpeq  29106  prlnghpg  29151  prlngpln3  29152  prlngex  29154  prlngmolem2  29156  incistruhgr  29370  upgrres1  29604  dfpth2  30019  usgr2pthlem  30053  iundisjf  32875  iundisjfi  33082  gsumfs2d  33322  cycpmfv3  33376  cyc3conja  33418  elrgspnlem4  33506  elrgspnsubrunlem2  33509  mxidlirredi  33699  qsdrngilem  33721  dflringlem2  33730  dflring3  33732  rsprprmprmidlb  33758  rprmirred  33766  rprmirredb  33767  1arithufdlem3  33781  dfufd2  33785  ply1dg3rt0irred  33819  ig1pmindeg  33837  selvascl  33852  esplyfv  33905  esplyfval3  33907  esplyfvn  33912  fldextrspunlsplem  34008  fldextrspunlsp  34009  submateqlem1  34142  submateqlem2  34143  elzrhunit  34312  qqhval2  34317  esumrnmpt2  34403  inelpisys  34489  nmulprop  36615  onint1  36883  mh-inf3sn  36976  lindsadd  38186  lindsenlbs  38188  poimirlem23  38216  poimirlem30  38223  dvasin  38277  areacirclem4  38284  pridlc3  38646  relogbzexpd  42667  dvrelog2b  42757  dvrelogpow2b  42759  aks4d1p1p4  42762  aks4d1p6  42772  aks6d1c7lem1  42871  nelsubginvcld  43194  nelsubgcld  43195  prjspersym  43265  prjspreln0  43267  prjspnvs  43278  rmspecsqrtnq  43559  rmspecnonsq  43560  pr2eldif1  44206  pr2eldif2  44207  disjf1o  45835  difmap  45849  difmapsn  45854  supminfxr2  46109  icoiccdif  46166  iccdificc  46181  climrec  46245  limciccioolb  46263  limcrecl  46271  sumnnodd  46272  lptioo2  46273  lptioo1  46274  limcicciooub  46277  lptre2pt  46280  reclimc  46293  cnrefiisplem  46469  icccncfext  46527  fperdvper  46559  dvnmul  46583  itgcoscmulx  46609  itgsincmulx  46614  stoweidlem34  46674  stoweidlem39  46679  stoweidlem57  46697  wallispi  46710  stirlinglem8  46721  dirkercncflem2  46744  dirkercncflem4  46746  fourierdlem38  46785  fourierdlem40  46787  fourierdlem42  46789  fourierdlem46  46792  fourierdlem53  46799  fourierdlem56  46802  fourierdlem58  46804  fourierdlem62  46808  fourierdlem74  46820  fourierdlem75  46821  fourierdlem76  46822  fourierdlem78  46824  fourierdlem93  46839  fourierdlem103  46849  fourierdlem104  46850  fouriersw  46871  elaa2  46874  etransc  46923  gsumge0cl  47011  sge0fodjrnlem  47056  iundjiun  47100  meadjiunlem  47105  meaiininclem  47126  caragendifcl  47154  caratheodorylem1  47166  hoidmvlelem1  47235  hoidmvlelem2  47236  hoidmvlelem4  47238  hspdifhsp  47256  hspmbllem2  47267  preimagelt  47339  preimalegt  47340  sqrtnegnre  47967  requad01  48309  dig1  49307