Theorem eldifd 3901

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3900. (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 3900	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ∖ cdif 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893

This theorem is referenced by:  rexdifi  4091  eqoreldif  4630  frd  5583  xpdifid  6128  funeldmdif  7996  ressuppssdif  8130  oaf1o  8493  findcard2d  9096  cantnflem1  9605  cantnflem2  9606  ttrcltr  9632  fin23lem26  10242  isf34lem4  10294  isfin7-2  10313  axdc3lem4  10370  axdc4lem  10372  ttukeylem7  10432  pwfseqlem1  10576  pwfseqlem3  10578  hashf1lem1  14412  seqcoll  14421  seqcoll2  14422  rlimcld2  15535  sumrblem  15668  fsumcvg  15669  fsumss  15682  incexclem  15796  prodrblem  15889  fprodcvg  15890  fprodss  15908  fprodn0f  15951  ruclem12  16203  sqrt2irr0  16213  coprmproddvdslem  16626  nnoddn2prmb  16779  prmreclem5  16886  ramub1lem1  16992  mreexd  17603  chnccats1  18586  chnccat  18587  frgpnabllem1  19843  gsumzaddlem  19891  gsum2d  19942  gsumxp2  19950  dmdprdsplitlem  20009  pgpfac1lem2  20047  pgpfac1lem3  20049  irredrmul  20402  lsppratlem3  21143  lbsextlem4  21155  psgnodpmr  21584  frlmsslsp  21790  regsep2  23355  1stckgen  23533  regr1lem  23718  opnsubg  24087  zcld  24793  recld2  24794  bcthlem4  25308  iundisj  25529  iblss2  25787  itgeqa  25795  limcnlp  25859  dvloglem  26629  dvlog2lem  26633  2irrexpq  26712  rtprmirr  26741  logbgcd1irr  26775  ressatans  26915  regamcl  27042  facgam  27047  wilthlem2  27050  2lgslem2  27376  noetasuplem4  27718  noetainflem4  27722  mulsval  28119  tgelrnln  28716  incistruhgr  29166  upgrres1  29400  dfpth2  29816  usgr2pthlem  29850  iundisjf  32678  iundisjfi  32888  gsumfs2d  33141  cycpmfv3  33195  cyc3conja  33237  elrgspnlem4  33325  elrgspnsubrunlem2  33328  mxidlirredi  33550  qsdrngilem  33573  rsprprmprmidlb  33602  rprmirred  33610  rprmirredb  33611  1arithufdlem3  33625  dfufd2  33629  ply1dg3rt0irred  33663  ig1pmindeg  33681  esplyfv  33733  esplyfval3  33735  esplyfvn  33740  fldextrspunlsplem  33837  fldextrspunlsp  33838  submateqlem1  33971  submateqlem2  33972  elzrhunit  34141  qqhval2  34146  esumrnmpt2  34232  inelpisys  34318  plymulx  34712  onint1  36651  mh-inf3sn  36744  lindsadd  37952  lindsenlbs  37954  poimirlem23  37982  poimirlem30  37989  dvasin  38043  areacirclem4  38050  pridlc3  38412  relogbzexpd  42433  dvrelog2b  42523  dvrelogpow2b  42525  aks4d1p1p4  42528  aks4d1p6  42538  aks6d1c7lem1  42637  nelsubginvcld  42959  nelsubgcld  42960  prjspersym  43058  prjspreln0  43060  prjspnvs  43071  rmspecsqrtnq  43356  rmspecnonsq  43357  pr2eldif1  44003  pr2eldif2  44004  disjf1o  45643  difmap  45658  difmapsn  45663  supminfxr2  45919  icoiccdif  45976  iccdificc  45991  climrec  46055  limciccioolb  46073  limcrecl  46081  sumnnodd  46082  lptioo2  46083  lptioo1  46084  limcicciooub  46087  lptre2pt  46090  reclimc  46103  cnrefiisplem  46279  icccncfext  46337  fperdvper  46369  dvnmul  46393  itgcoscmulx  46419  itgsincmulx  46424  stoweidlem34  46484  stoweidlem39  46489  stoweidlem57  46507  wallispi  46520  stirlinglem8  46531  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem38  46595  fourierdlem40  46597  fourierdlem42  46599  fourierdlem46  46602  fourierdlem53  46609  fourierdlem56  46612  fourierdlem58  46614  fourierdlem62  46618  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem78  46634  fourierdlem93  46649  fourierdlem103  46659  fourierdlem104  46660  fouriersw  46681  elaa2  46684  etransc  46733  gsumge0cl  46821  sge0fodjrnlem  46866  iundjiun  46910  meadjiunlem  46915  meaiininclem  46936  caragendifcl  46964  caratheodorylem1  46976  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem4  47048  hspdifhsp  47066  hspmbllem2  47077  preimagelt  47149  preimalegt  47150  sqrtnegnre  47771  requad01  48113  dig1  49100