Theorem eldifd 3914

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3900

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906

This theorem is referenced by:  rexdifi  4101  eqoreldif  4637  frd  5576  xpdifid  6117  funeldmdif  7983  ressuppssdif  8118  oaf1o  8481  findcard2d  9080  cantnflem1  9585  cantnflem2  9586  ttrcltr  9612  fin23lem26  10219  isf34lem4  10271  isfin7-2  10290  axdc3lem4  10347  axdc4lem  10349  ttukeylem7  10409  pwfseqlem1  10552  pwfseqlem3  10554  hashf1lem1  14362  seqcoll  14371  seqcoll2  14372  rlimcld2  15485  sumrblem  15618  fsumcvg  15619  fsumss  15632  incexclem  15743  prodrblem  15836  fprodcvg  15837  fprodss  15855  fprodn0f  15898  ruclem12  16150  sqrt2irr0  16160  coprmproddvdslem  16573  nnoddn2prmb  16725  prmreclem5  16832  ramub1lem1  16938  mreexd  17548  frgpnabllem1  19752  gsumzaddlem  19800  gsum2d  19851  gsumxp2  19859  dmdprdsplitlem  19918  pgpfac1lem2  19956  pgpfac1lem3  19958  irredrmul  20312  lsppratlem3  21056  lbsextlem4  21068  psgnodpmr  21497  frlmsslsp  21703  regsep2  23261  1stckgen  23439  regr1lem  23624  opnsubg  23993  zcld  24700  recld2  24701  bcthlem4  25225  iundisj  25447  iblss2  25705  itgeqa  25713  limcnlp  25777  dvloglem  26555  dvlog2lem  26559  2irrexpq  26638  rtprmirr  26668  logbgcd1irr  26702  ressatans  26842  regamcl  26969  facgam  26974  wilthlem2  26977  2lgslem2  27304  noetasuplem4  27646  noetainflem4  27650  mulsval  28017  tgelrnln  28575  incistruhgr  29024  upgrres1  29258  dfpth2  29674  usgr2pthlem  29708  iundisjf  32533  iundisjfi  32740  chnccats1  32958  gsumfs2d  33009  cycpmfv3  33058  cyc3conja  33100  elrgspnlem4  33186  elrgspnsubrunlem2  33189  mxidlirredi  33409  qsdrngilem  33432  rsprprmprmidlb  33461  rprmirred  33469  rprmirredb  33470  1arithufdlem3  33484  dfufd2  33488  ply1dg3rt0irred  33519  ig1pmindeg  33535  fldextrspunlsplem  33646  fldextrspunlsp  33647  submateqlem1  33780  submateqlem2  33781  elzrhunit  33950  qqhval2  33955  esumrnmpt2  34041  inelpisys  34127  plymulx  34522  onint1  36433  lindsadd  37603  lindsenlbs  37605  poimirlem23  37633  poimirlem30  37640  dvasin  37694  areacirclem4  37701  pridlc3  38063  relogbzexpd  41958  dvrelog2b  42049  dvrelogpow2b  42051  aks4d1p1p4  42054  aks4d1p6  42064  aks6d1c7lem1  42163  nelsubginvcld  42479  nelsubgcld  42480  prjspersym  42590  prjspreln0  42592  prjspnvs  42603  rmspecsqrtnq  42889  rmspecnonsq  42890  pr2eldif1  43537  pr2eldif2  43538  disjf1o  45179  difmap  45195  difmapsn  45200  supminfxr2  45458  icoiccdif  45515  iccdificc  45530  climrec  45594  limciccioolb  45612  limcrecl  45620  sumnnodd  45621  lptioo2  45622  lptioo1  45623  limcicciooub  45628  lptre2pt  45631  reclimc  45644  cnrefiisplem  45820  icccncfext  45878  fperdvper  45910  dvnmul  45934  itgcoscmulx  45960  itgsincmulx  45965  stoweidlem34  46025  stoweidlem39  46030  stoweidlem57  46048  wallispi  46061  stirlinglem8  46072  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem38  46136  fourierdlem40  46138  fourierdlem42  46140  fourierdlem46  46143  fourierdlem53  46150  fourierdlem56  46153  fourierdlem58  46155  fourierdlem62  46159  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem93  46190  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  elaa2  46225  etransc  46274  gsumge0cl  46362  sge0fodjrnlem  46407  iundjiun  46451  meadjiunlem  46456  meaiininclem  46477  caragendifcl  46505  caratheodorylem1  46517  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem4  46589  hspdifhsp  46607  hspmbllem2  46618  preimagelt  46690  preimalegt  46691  sqrtnegnre  47301  requad01  47615  dig1  48603