Theorem eldifd 3899

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891

This theorem is referenced by:  rexdifi  4081  eqoreldif  4621  frd  5549  xpdifid  6076  funeldmdif  7898  ressuppssdif  8010  oaf1o  8403  findcard2d  8958  cantnflem1  9456  cantnflem2  9457  ttrcltr  9483  fin23lem26  10090  isf34lem4  10142  isfin7-2  10161  axdc3lem4  10218  axdc4lem  10220  ttukeylem7  10280  pwfseqlem1  10423  pwfseqlem3  10425  hashf1lem1  14177  hashf1lem1OLD  14178  seqcoll  14187  seqcoll2  14188  rlimcld2  15296  sumrblem  15432  fsumcvg  15433  fsumss  15446  incexclem  15557  prodrblem  15648  fprodcvg  15649  fprodss  15667  fprodn0f  15710  ruclem12  15959  sqrt2irr0  15969  coprmproddvdslem  16376  nnoddn2prmb  16523  prmreclem5  16630  ramub1lem1  16736  mreexd  17360  frgpnabllem1  19483  gsumzaddlem  19531  gsum2d  19582  gsumxp2  19590  dmdprdsplitlem  19649  pgpfac1lem2  19687  pgpfac1lem3  19689  irredrmul  19958  lsppratlem3  20420  lbsextlem4  20432  psgnodpmr  20804  frlmsslsp  21012  regsep2  22536  1stckgen  22714  regr1lem  22899  opnsubg  23268  zcld  23985  recld2  23986  bcthlem4  24500  iundisj  24721  iblss2  24979  itgeqa  24987  limcnlp  25051  dvloglem  25812  dvlog2lem  25816  2irrexpq  25894  logbgcd1irr  25953  ressatans  26093  regamcl  26219  facgam  26224  wilthlem2  26227  2lgslem2  26552  tgelrnln  27000  incistruhgr  27458  upgrres1  27689  usgr2pthlem  28140  iundisjf  30937  iundisjfi  31126  cycpmfv3  31391  cyc3conja  31433  submateqlem1  31766  submateqlem2  31767  elzrhunit  31938  qqhval2  31941  esumrnmpt2  32045  inelpisys  32131  plymulx  32536  noetasuplem4  33948  noetainflem4  33952  onint1  34647  lindsadd  35779  lindsenlbs  35781  poimirlem23  35809  poimirlem30  35816  dvasin  35870  areacirclem4  35877  pridlc3  36240  relogbzexpd  39990  dvrelog2b  40081  dvrelogpow2b  40083  aks4d1p1p4  40086  aks4d1p6  40096  nelsubginvcld  40227  nelsubgcld  40228  rtprmirr  40354  prjspersym  40453  prjspreln0  40455  prjspvs  40456  prjspnvs  40466  prjcrv0  40477  rmspecsqrtnq  40735  rmspecnonsq  40736  pr2eldif1  41168  pr2eldif2  41169  disjf1o  42736  difmap  42754  difmapsn  42759  supminfxr2  43016  icoiccdif  43069  iccdificc  43084  climrec  43151  limciccioolb  43169  limcrecl  43177  sumnnodd  43178  lptioo2  43179  lptioo1  43180  limcicciooub  43185  lptre2pt  43188  reclimc  43201  cnrefiisplem  43377  icccncfext  43435  fperdvper  43467  dvnmul  43491  itgcoscmulx  43517  itgsincmulx  43522  stoweidlem34  43582  stoweidlem39  43587  stoweidlem57  43605  wallispi  43618  stirlinglem8  43629  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem38  43693  fourierdlem40  43695  fourierdlem42  43697  fourierdlem46  43700  fourierdlem53  43707  fourierdlem56  43710  fourierdlem58  43712  fourierdlem62  43716  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem78  43732  fourierdlem93  43747  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  elaa2  43782  etransc  43831  gsumge0cl  43916  sge0fodjrnlem  43961  iundjiun  44005  meadjiunlem  44010  meaiininclem  44031  caragendifcl  44059  caratheodorylem1  44071  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem4  44143  hspdifhsp  44161  hspmbllem2  44172  preimagelt  44244  preimalegt  44245  sqrtnegnre  44810  requad01  45084  dig1  45965