Theorem eldifd 3913

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-dif 3905

This theorem is referenced by:  rexdifi  4103  eqoreldif  4643  frd  5582  xpdifid  6127  funeldmdif  7994  ressuppssdif  8129  oaf1o  8492  findcard2d  9095  cantnflem1  9602  cantnflem2  9603  ttrcltr  9629  fin23lem26  10239  isf34lem4  10291  isfin7-2  10310  axdc3lem4  10367  axdc4lem  10369  ttukeylem7  10429  pwfseqlem1  10573  pwfseqlem3  10575  hashf1lem1  14382  seqcoll  14391  seqcoll2  14392  rlimcld2  15505  sumrblem  15638  fsumcvg  15639  fsumss  15652  incexclem  15763  prodrblem  15856  fprodcvg  15857  fprodss  15875  fprodn0f  15918  ruclem12  16170  sqrt2irr0  16180  coprmproddvdslem  16593  nnoddn2prmb  16745  prmreclem5  16852  ramub1lem1  16958  mreexd  17569  chnccats1  18552  chnccat  18553  frgpnabllem1  19806  gsumzaddlem  19854  gsum2d  19905  gsumxp2  19913  dmdprdsplitlem  19972  pgpfac1lem2  20010  pgpfac1lem3  20012  irredrmul  20367  lsppratlem3  21108  lbsextlem4  21120  psgnodpmr  21549  frlmsslsp  21755  regsep2  23324  1stckgen  23502  regr1lem  23687  opnsubg  24056  zcld  24762  recld2  24763  bcthlem4  25287  iundisj  25509  iblss2  25767  itgeqa  25775  limcnlp  25839  dvloglem  26617  dvlog2lem  26621  2irrexpq  26700  rtprmirr  26730  logbgcd1irr  26764  ressatans  26904  regamcl  27031  facgam  27036  wilthlem2  27039  2lgslem2  27366  noetasuplem4  27708  noetainflem4  27712  mulsval  28109  tgelrnln  28706  incistruhgr  29156  upgrres1  29390  dfpth2  29806  usgr2pthlem  29840  iundisjf  32667  iundisjfi  32878  gsumfs2d  33146  cycpmfv3  33199  cyc3conja  33241  elrgspnlem4  33329  elrgspnsubrunlem2  33332  mxidlirredi  33554  qsdrngilem  33577  rsprprmprmidlb  33606  rprmirred  33614  rprmirredb  33615  1arithufdlem3  33629  dfufd2  33633  ply1dg3rt0irred  33667  ig1pmindeg  33685  esplyfv  33730  esplyfval3  33732  esplyfvn  33735  fldextrspunlsplem  33832  fldextrspunlsp  33833  submateqlem1  33966  submateqlem2  33967  elzrhunit  34136  qqhval2  34141  esumrnmpt2  34227  inelpisys  34313  plymulx  34707  onint1  36645  lindsadd  37816  lindsenlbs  37818  poimirlem23  37846  poimirlem30  37853  dvasin  37907  areacirclem4  37914  pridlc3  38276  relogbzexpd  42297  dvrelog2b  42388  dvrelogpow2b  42390  aks4d1p1p4  42393  aks4d1p6  42403  aks6d1c7lem1  42502  nelsubginvcld  42818  nelsubgcld  42819  prjspersym  42917  prjspreln0  42919  prjspnvs  42930  rmspecsqrtnq  43215  rmspecnonsq  43216  pr2eldif1  43862  pr2eldif2  43863  disjf1o  45502  difmap  45518  difmapsn  45523  supminfxr2  45780  icoiccdif  45837  iccdificc  45852  climrec  45916  limciccioolb  45934  limcrecl  45942  sumnnodd  45943  lptioo2  45944  lptioo1  45945  limcicciooub  45948  lptre2pt  45951  reclimc  45964  cnrefiisplem  46140  icccncfext  46198  fperdvper  46230  dvnmul  46254  itgcoscmulx  46280  itgsincmulx  46285  stoweidlem34  46345  stoweidlem39  46350  stoweidlem57  46368  wallispi  46381  stirlinglem8  46392  dirkercncflem2  46415  dirkercncflem4  46417  fourierdlem38  46456  fourierdlem40  46458  fourierdlem42  46460  fourierdlem46  46463  fourierdlem53  46470  fourierdlem56  46473  fourierdlem58  46475  fourierdlem62  46479  fourierdlem74  46491  fourierdlem75  46492  fourierdlem76  46493  fourierdlem78  46495  fourierdlem93  46510  fourierdlem103  46520  fourierdlem104  46521  fouriersw  46542  elaa2  46545  etransc  46594  gsumge0cl  46682  sge0fodjrnlem  46727  iundjiun  46771  meadjiunlem  46776  meaiininclem  46797  caragendifcl  46825  caratheodorylem1  46837  hoidmvlelem1  46906  hoidmvlelem2  46907  hoidmvlelem4  46909  hspdifhsp  46927  hspmbllem2  46938  preimagelt  47010  preimalegt  47011  sqrtnegnre  47620  requad01  47934  dig1  48921