Theorem eldifd 3916

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2143   ∖ cdif 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908

This theorem is used by:  rexdifi  4104  eqoreldif  4651  frd  5618  xpdifid  6165  xpdifcnvepel  6166  funeldmdif  8041  ressuppssdif  8177  oaf1o  8544  findcard2d  9147  cantnflem1  9654  cantnflem2  9655  ttrcltr  9681  fin23lem26  10313  isf34lem4  10365  isfin7-2  10384  axdc3lem4  10441  axdc4lem  10443  ttukeylem7  10503  pwfseqlem1  10647  pwfseqlem3  10649  hashf1lem1  14497  seqcoll  14506  seqcoll2  14507  rlimcld2  15634  sumrblem  15767  fsumcvg  15768  fsumss  15781  incexclem  15895  prodrblem  15988  fprodcvg  15989  fprodss  16007  fprodn0f  16050  ruclem12  16301  sqrt2irr0  16311  coprmproddvdslem  16724  nnoddn2prmb  16877  prmreclem5  16984  ramub1lem1  17090  mreexd  17702  chnccats1  18685  chnccat  18686  frgpnabllem1  19947  gsumzaddlem  19995  gsum2d  20046  gsumxp2  20054  dmdprdsplitlem  20113  pgpfac1lem2  20151  pgpfac1lem3  20153  irredrmul  20514  lsppratlem3  21282  lbsextlem4  21294  cmprmidlmcl  21484  prmidlsubm  21496  psgnodpmr  21749  frlmsslsp  21955  regsep2  23542  1stckgen  23720  regr1lem  23905  opnsubg  24274  zcld  24980  recld2  24981  bcthlem4  25495  iundisj  25716  iblss2  25974  itgeqa  25982  limcnlp  26046  plymulidp  26452  dvloglem  26822  dvlog2lem  26826  2irrexpq  26905  rtprmirr  26934  logbgcd1irr  26968  ressatans  27108  regamcl  27234  facgam  27239  wilthlem2  27242  2lgslem2  27568  noetasuplem4  27909  noetainflem4  27913  mulsval  28311  tgelrnln  28912  tglnpt4  28937  tgelrnpln  29067  lnincplng  29075  plngcplem  29076  plngrotlem1  29078  plngrotlem2  29079  lnssplnglem  29082  lnssplng  29083  nhpmirhp  29089  perpeq  29160  prlnghpg  29205  dfprlng2  29206  prlngpln3  29208  prlngex  29210  prlngmolem2  29212  prlngmo2  29215  prlngpln4  29217  symquadprlng  29221  prlngsymquadlem  29222  quadcgrprlng  29225  incistruhgr  29438  upgrres1  29672  dfpth2  30087  usgr2pthlem  30121  iundisjf  32943  iundisjfi  33150  gsumfs2d  33390  cycpmfv3  33444  cyc3conja  33486  elrgspnlem4  33574  elrgspnsubrunlem2  33577  mxidlirredi  33763  qsdrngilem  33785  dflringlem2  33794  dflring3  33796  rsprprmprmidlb  33822  rprmirred  33830  rprmirredb  33831  1arithufdlem3  33845  dfufd2  33849  ply1dg3rt0irred  33883  ig1pmindeg  33901  selvascl  33916  esplyfv  33969  esplyfval3  33971  esplyfvn  33976  fldextrspunlsplem  34072  fldextrspunlsp  34073  submateqlem1  34206  submateqlem2  34207  elzrhunit  34376  qqhval2  34381  esumrnmpt2  34467  inelpisys  34553  nmulprop  36690  onint1  36988  mh-inf3sn  37081  lindsadd  38292  lindsenlbs  38294  poimirlem23  38322  poimirlem30  38329  dvasin  38383  areacirclem4  38390  pridlc3  38752  relogbzexpd  42771  dvrelog2b  42861  dvrelogpow2b  42863  aks4d1p1p4  42866  aks4d1p6  42876  aks6d1c7lem1  42975  nelsubginvcld  43298  nelsubgcld  43299  prjspersym  43367  prjspreln0  43369  prjspnvs  43380  rmspecsqrtnq  43661  rmspecnonsq  43662  pr2eldif1  44308  pr2eldif2  44309  disjf1o  45937  difmap  45951  difmapsn  45956  supminfxr2  46211  icoiccdif  46268  iccdificc  46283  climrec  46347  limciccioolb  46365  limcrecl  46373  sumnnodd  46374  lptioo2  46375  lptioo1  46376  limcicciooub  46379  lptre2pt  46382  reclimc  46395  cnrefiisplem  46571  icccncfext  46629  fperdvper  46661  dvnmul  46685  itgcoscmulx  46711  itgsincmulx  46716  stoweidlem34  46776  stoweidlem39  46781  stoweidlem57  46799  wallispi  46812  stirlinglem8  46823  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem38  46887  fourierdlem40  46889  fourierdlem42  46891  fourierdlem46  46894  fourierdlem53  46901  fourierdlem56  46904  fourierdlem58  46906  fourierdlem62  46910  fourierdlem74  46922  fourierdlem75  46923  fourierdlem76  46924  fourierdlem78  46926  fourierdlem93  46941  fourierdlem103  46951  fourierdlem104  46952  fouriersw  46973  elaa2  46976  etransc  47025  gsumge0cl  47113  sge0fodjrnlem  47158  iundjiun  47202  meadjiunlem  47207  meaiininclem  47228  caragendifcl  47256  caratheodorylem1  47268  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem4  47340  hspdifhsp  47358  hspmbllem2  47369  preimagelt  47441  preimalegt  47442  sqrtnegnre  48072  requad01  48414  dig1  49416