Theorem eldifd 3917

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909

This theorem is used by:  rexdifi  4104  eqoreldif  4653  frd  5620  xpdifid  6167  xpdifcnvepel  6168  funeldmdif  8051  ressuppssdif  8187  oaf1o  8554  findcard2d  9158  cantnflem1  9665  cantnflem2  9666  ttrcltr  9692  fin23lem26  10324  isf34lem4  10376  isfin7-2  10395  axdc3lem4  10452  axdc4lem  10454  ttukeylem7  10514  pwfseqlem1  10662  pwfseqlem3  10664  hashf1lem1  14514  seqcoll  14523  seqcoll2  14524  rlimcld2  15657  sumrblem  15789  fsumcvg  15790  fsumss  15803  incexclem  15917  prodrblem  16010  fprodcvg  16011  fprodss  16029  fprodn0f  16072  ruclem12  16323  sqrt2irr0  16333  coprmproddvdslem  16746  nnoddn2prmb  16899  prmreclem5  17006  ramub1lem1  17112  mreexd  17724  chnccats1  18707  chnccat  18708  frgpnabllem1  19991  gsumzaddlem  20039  gsum2d  20090  gsumxp2  20098  dmdprdsplitlem  20157  pgpfac1lem2  20195  pgpfac1lem3  20197  irredrmul  20559  lsppratlem3  21327  lbsextlem4  21339  cmprmidlmcl  21529  prmidlsubm  21541  psgnodpmr  21794  frlmsslsp  22000  regsep2  23587  1stckgen  23766  regr1lem  23951  opnsubg  24320  zcld  25026  recld2  25027  bcthlem4  25541  iundisj  25762  iblss2  26020  itgeqa  26028  limcnlp  26092  plymulidp  26498  dvloglem  26868  dvlog2lem  26872  2irrexpq  26951  rtprmirr  26980  logbgcd1irr  27014  ressatans  27154  regamcl  27280  facgam  27285  wilthlem2  27288  2lgslem2  27614  noetasuplem4  27955  noetainflem4  27959  mulsval  28357  tgelrnln  28958  tglnpt4  28983  tgelrnpln  29113  lnincplng  29121  plngcplem  29122  plngrotlem1  29124  plngrotlem2  29125  lnssplnglem  29128  lnssplng  29129  nhpmirhp  29135  perpeq  29206  tgaaddcpbllem1  29207  tgaaddcpbl  29210  prlnghpg  29255  dfprlng2  29256  prlngpln3  29258  prlngex  29260  prlngmolem2  29262  prlngmo2  29265  prlngpln4  29267  symquadprlng  29271  prlngsymquadlem  29272  quadcgrprlng  29275  incistruhgr  29488  upgrres1  29725  dfpth2  30145  usgr2pthlem  30180  iundisjf  33009  iundisjfi  33215  gsumfs2d  33449  cycpmfv3  33503  cyc3conja  33545  elrgspnlem4  33633  elrgspnsubrunlem2  33636  mxidlirredi  33822  qsdrngilem  33844  dflringlem2  33853  dflring3  33855  rsprprmprmidlb  33881  rprmirred  33889  rprmirredb  33890  1arithufdlem3  33904  dfufd2  33908  ply1dg3rt0irred  33942  ig1pmindeg  33960  selvascl  33975  esplyfv  34028  esplyfval3  34030  esplyfvn  34035  fldextrspunlsplem  34131  fldextrspunlsp  34132  submateqlem1  34265  submateqlem2  34266  elzrhunit  34435  qqhval2  34440  esumrnmpt2  34526  inelpisys  34613  nmulprop  36723  onint1  37021  mh-inf3sn  37114  lindsadd  38325  lindsenlbs  38327  poimirlem23  38355  poimirlem30  38362  dvasin  38416  areacirclem4  38423  pridlc3  38786  relogbzexpd  42805  dvrelog2b  42895  dvrelogpow2b  42897  aks4d1p1p4  42900  aks4d1p6  42910  aks6d1c7lem1  43009  nelsubginvcld  43347  nelsubgcld  43348  prjspersym  43416  prjspreln0  43418  prjspnvs  43429  rmspecsqrtnq  43710  rmspecnonsq  43711  pr2eldif1  44357  pr2eldif2  44358  disjf1o  45986  difmap  46000  difmapsn  46005  supminfxr2  46260  icoiccdif  46317  iccdificc  46332  climrec  46396  limciccioolb  46414  limcrecl  46422  sumnnodd  46423  lptioo2  46424  lptioo1  46425  limcicciooub  46428  lptre2pt  46431  reclimc  46444  cnrefiisplem  46620  icccncfext  46678  fperdvper  46710  dvnmul  46734  itgcoscmulx  46760  itgsincmulx  46765  stoweidlem34  46825  stoweidlem39  46830  stoweidlem57  46848  wallispi  46861  stirlinglem8  46872  dirkercncflem2  46895  dirkercncflem4  46897  fourierdlem38  46936  fourierdlem40  46938  fourierdlem42  46940  fourierdlem46  46943  fourierdlem53  46950  fourierdlem56  46953  fourierdlem58  46955  fourierdlem62  46959  fourierdlem74  46971  fourierdlem75  46972  fourierdlem76  46973  fourierdlem78  46975  fourierdlem93  46990  fourierdlem103  47000  fourierdlem104  47001  fouriersw  47022  elaa2  47025  etransc  47074  gsumge0cl  47162  sge0fodjrnlem  47207  iundjiun  47251  meadjiunlem  47256  meaiininclem  47277  caragendifcl  47305  caratheodorylem1  47317  hoidmvlelem1  47386  hoidmvlelem2  47387  hoidmvlelem4  47389  hspdifhsp  47407  hspmbllem2  47418  preimagelt  47490  preimalegt  47491  sqrtnegnre  48121  requad01  48463  dig1  49464