Theorem eldifd 3987

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979

This theorem is referenced by:  rexdifi  4173  eqoreldif  4708  frd  5656  xpdifid  6199  funeldmdif  8089  ressuppssdif  8226  oaf1o  8619  findcard2d  9232  cantnflem1  9758  cantnflem2  9759  ttrcltr  9785  fin23lem26  10394  isf34lem4  10446  isfin7-2  10465  axdc3lem4  10522  axdc4lem  10524  ttukeylem7  10584  pwfseqlem1  10727  pwfseqlem3  10729  hashf1lem1  14504  seqcoll  14513  seqcoll2  14514  rlimcld2  15624  sumrblem  15759  fsumcvg  15760  fsumss  15773  incexclem  15884  prodrblem  15977  fprodcvg  15978  fprodss  15996  fprodn0f  16039  ruclem12  16289  sqrt2irr0  16299  coprmproddvdslem  16709  nnoddn2prmb  16860  prmreclem5  16967  ramub1lem1  17073  mreexd  17700  frgpnabllem1  19915  gsumzaddlem  19963  gsum2d  20014  gsumxp2  20022  dmdprdsplitlem  20081  pgpfac1lem2  20119  pgpfac1lem3  20121  irredrmul  20453  lsppratlem3  21174  lbsextlem4  21186  psgnodpmr  21631  frlmsslsp  21839  regsep2  23405  1stckgen  23583  regr1lem  23768  opnsubg  24137  zcld  24854  recld2  24855  bcthlem4  25380  iundisj  25602  iblss2  25861  itgeqa  25869  limcnlp  25933  dvloglem  26708  dvlog2lem  26712  2irrexpq  26791  rtprmirr  26821  logbgcd1irr  26855  ressatans  26995  regamcl  27122  facgam  27127  wilthlem2  27130  2lgslem2  27457  noetasuplem4  27799  noetainflem4  27803  mulsval  28153  tgelrnln  28656  incistruhgr  29114  upgrres1  29348  usgr2pthlem  29799  iundisjf  32611  iundisjfi  32801  cycpmfv3  33108  cyc3conja  33150  mxidlirredi  33464  qsdrngilem  33487  rsprprmprmidlb  33516  rprmirred  33524  rprmirredb  33525  1arithufdlem3  33539  dfufd2  33543  ply1dg3rt0irred  33572  ig1pmindeg  33587  submateqlem1  33753  submateqlem2  33754  elzrhunit  33925  qqhval2  33928  esumrnmpt2  34032  inelpisys  34118  plymulx  34525  onint1  36415  lindsadd  37573  lindsenlbs  37575  poimirlem23  37603  poimirlem30  37610  dvasin  37664  areacirclem4  37671  pridlc3  38033  relogbzexpd  41931  dvrelog2b  42023  dvrelogpow2b  42025  aks4d1p1p4  42028  aks4d1p6  42038  aks6d1c7lem1  42137  nelsubginvcld  42451  nelsubgcld  42452  prjspersym  42562  prjspreln0  42564  prjspnvs  42575  rmspecsqrtnq  42862  rmspecnonsq  42863  pr2eldif1  43516  pr2eldif2  43517  disjf1o  45098  difmap  45114  difmapsn  45119  supminfxr2  45384  icoiccdif  45442  iccdificc  45457  climrec  45524  limciccioolb  45542  limcrecl  45550  sumnnodd  45551  lptioo2  45552  lptioo1  45553  limcicciooub  45558  lptre2pt  45561  reclimc  45574  cnrefiisplem  45750  icccncfext  45808  fperdvper  45840  dvnmul  45864  itgcoscmulx  45890  itgsincmulx  45895  stoweidlem34  45955  stoweidlem39  45960  stoweidlem57  45978  wallispi  45991  stirlinglem8  46002  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem38  46066  fourierdlem40  46068  fourierdlem42  46070  fourierdlem46  46073  fourierdlem53  46080  fourierdlem56  46083  fourierdlem58  46085  fourierdlem62  46089  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  elaa2  46155  etransc  46204  gsumge0cl  46292  sge0fodjrnlem  46337  iundjiun  46381  meadjiunlem  46386  meaiininclem  46407  caragendifcl  46435  caratheodorylem1  46447  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem4  46519  hspdifhsp  46537  hspmbllem2  46548  preimagelt  46620  preimalegt  46621  sqrtnegnre  47222  requad01  47495  dig1  48342