Theorem eldifd 3973

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965

This theorem is referenced by:  rexdifi  4159  eqoreldif  4689  frd  5644  xpdifid  6189  funeldmdif  8071  ressuppssdif  8208  oaf1o  8599  findcard2d  9204  cantnflem1  9726  cantnflem2  9727  ttrcltr  9753  fin23lem26  10362  isf34lem4  10414  isfin7-2  10433  axdc3lem4  10490  axdc4lem  10492  ttukeylem7  10552  pwfseqlem1  10695  pwfseqlem3  10697  hashf1lem1  14490  seqcoll  14499  seqcoll2  14500  rlimcld2  15610  sumrblem  15743  fsumcvg  15744  fsumss  15757  incexclem  15868  prodrblem  15961  fprodcvg  15962  fprodss  15980  fprodn0f  16023  ruclem12  16273  sqrt2irr0  16283  coprmproddvdslem  16695  nnoddn2prmb  16846  prmreclem5  16953  ramub1lem1  17059  mreexd  17686  frgpnabllem1  19905  gsumzaddlem  19953  gsum2d  20004  gsumxp2  20012  dmdprdsplitlem  20071  pgpfac1lem2  20109  pgpfac1lem3  20111  irredrmul  20443  lsppratlem3  21168  lbsextlem4  21180  psgnodpmr  21625  frlmsslsp  21833  regsep2  23399  1stckgen  23577  regr1lem  23762  opnsubg  24131  zcld  24848  recld2  24849  bcthlem4  25374  iundisj  25596  iblss2  25855  itgeqa  25863  limcnlp  25927  dvloglem  26704  dvlog2lem  26708  2irrexpq  26787  rtprmirr  26817  logbgcd1irr  26851  ressatans  26991  regamcl  27118  facgam  27123  wilthlem2  27126  2lgslem2  27453  noetasuplem4  27795  noetainflem4  27799  mulsval  28149  tgelrnln  28652  incistruhgr  29110  upgrres1  29344  usgr2pthlem  29795  iundisjf  32608  iundisjfi  32803  gsumfs2d  33040  cycpmfv3  33117  cyc3conja  33159  elrgspnlem4  33234  mxidlirredi  33478  qsdrngilem  33501  rsprprmprmidlb  33530  rprmirred  33538  rprmirredb  33539  1arithufdlem3  33553  dfufd2  33557  ply1dg3rt0irred  33586  ig1pmindeg  33601  submateqlem1  33767  submateqlem2  33768  elzrhunit  33939  qqhval2  33944  esumrnmpt2  34048  inelpisys  34134  plymulx  34541  onint1  36431  lindsadd  37599  lindsenlbs  37601  poimirlem23  37629  poimirlem30  37636  dvasin  37690  areacirclem4  37697  pridlc3  38059  relogbzexpd  41956  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p6  42062  aks6d1c7lem1  42161  nelsubginvcld  42482  nelsubgcld  42483  prjspersym  42593  prjspreln0  42595  prjspnvs  42606  rmspecsqrtnq  42893  rmspecnonsq  42894  pr2eldif1  43543  pr2eldif2  43544  disjf1o  45133  difmap  45149  difmapsn  45154  supminfxr2  45418  icoiccdif  45476  iccdificc  45491  climrec  45558  limciccioolb  45576  limcrecl  45584  sumnnodd  45585  lptioo2  45586  lptioo1  45587  limcicciooub  45592  lptre2pt  45595  reclimc  45608  cnrefiisplem  45784  icccncfext  45842  fperdvper  45874  dvnmul  45898  itgcoscmulx  45924  itgsincmulx  45929  stoweidlem34  45989  stoweidlem39  45994  stoweidlem57  46012  wallispi  46025  stirlinglem8  46036  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem38  46100  fourierdlem40  46102  fourierdlem42  46104  fourierdlem46  46107  fourierdlem53  46114  fourierdlem56  46117  fourierdlem58  46119  fourierdlem62  46123  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem93  46154  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  elaa2  46189  etransc  46238  gsumge0cl  46326  sge0fodjrnlem  46371  iundjiun  46415  meadjiunlem  46420  meaiininclem  46441  caragendifcl  46469  caratheodorylem1  46481  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem4  46553  hspdifhsp  46571  hspmbllem2  46582  preimagelt  46654  preimalegt  46655  sqrtnegnre  47256  requad01  47545  dig1  48457