Theorem eldifd 3922

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

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

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 3446  df-dif 3914

This theorem is referenced by:  rexdifi  4109  eqoreldif  4645  frd  5588  xpdifid  6129  funeldmdif  8006  ressuppssdif  8141  oaf1o  8504  findcard2d  9107  cantnflem1  9618  cantnflem2  9619  ttrcltr  9645  fin23lem26  10254  isf34lem4  10306  isfin7-2  10325  axdc3lem4  10382  axdc4lem  10384  ttukeylem7  10444  pwfseqlem1  10587  pwfseqlem3  10589  hashf1lem1  14396  seqcoll  14405  seqcoll2  14406  rlimcld2  15520  sumrblem  15653  fsumcvg  15654  fsumss  15667  incexclem  15778  prodrblem  15871  fprodcvg  15872  fprodss  15890  fprodn0f  15933  ruclem12  16185  sqrt2irr0  16195  coprmproddvdslem  16608  nnoddn2prmb  16760  prmreclem5  16867  ramub1lem1  16973  mreexd  17583  frgpnabllem1  19787  gsumzaddlem  19835  gsum2d  19886  gsumxp2  19894  dmdprdsplitlem  19953  pgpfac1lem2  19991  pgpfac1lem3  19993  irredrmul  20347  lsppratlem3  21091  lbsextlem4  21103  psgnodpmr  21532  frlmsslsp  21738  regsep2  23296  1stckgen  23474  regr1lem  23659  opnsubg  24028  zcld  24735  recld2  24736  bcthlem4  25260  iundisj  25482  iblss2  25740  itgeqa  25748  limcnlp  25812  dvloglem  26590  dvlog2lem  26594  2irrexpq  26673  rtprmirr  26703  logbgcd1irr  26737  ressatans  26877  regamcl  27004  facgam  27009  wilthlem2  27012  2lgslem2  27339  noetasuplem4  27681  noetainflem4  27685  mulsval  28052  tgelrnln  28610  incistruhgr  29059  upgrres1  29293  dfpth2  29709  usgr2pthlem  29743  iundisjf  32568  iundisjfi  32769  chnccats1  32987  gsumfs2d  33038  cycpmfv3  33087  cyc3conja  33129  elrgspnlem4  33212  elrgspnsubrunlem2  33215  mxidlirredi  33435  qsdrngilem  33458  rsprprmprmidlb  33487  rprmirred  33495  rprmirredb  33496  1arithufdlem3  33510  dfufd2  33514  ply1dg3rt0irred  33544  ig1pmindeg  33560  fldextrspunlsplem  33661  fldextrspunlsp  33662  submateqlem1  33790  submateqlem2  33791  elzrhunit  33960  qqhval2  33965  esumrnmpt2  34051  inelpisys  34137  plymulx  34532  onint1  36430  lindsadd  37600  lindsenlbs  37602  poimirlem23  37630  poimirlem30  37637  dvasin  37691  areacirclem4  37698  pridlc3  38060  relogbzexpd  41956  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p6  42062  aks6d1c7lem1  42161  nelsubginvcld  42477  nelsubgcld  42478  prjspersym  42588  prjspreln0  42590  prjspnvs  42601  rmspecsqrtnq  42887  rmspecnonsq  42888  pr2eldif1  43536  pr2eldif2  43537  disjf1o  45178  difmap  45194  difmapsn  45199  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  48590