Theorem eldifd 3914

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

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

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 3444  df-dif 3906

This theorem is referenced by:  rexdifi  4104  eqoreldif  4644  frd  5591  xpdifid  6136  funeldmdif  8004  ressuppssdif  8139  oaf1o  8502  findcard2d  9105  cantnflem1  9612  cantnflem2  9613  ttrcltr  9639  fin23lem26  10249  isf34lem4  10301  isfin7-2  10320  axdc3lem4  10377  axdc4lem  10379  ttukeylem7  10439  pwfseqlem1  10583  pwfseqlem3  10585  hashf1lem1  14392  seqcoll  14401  seqcoll2  14402  rlimcld2  15515  sumrblem  15648  fsumcvg  15649  fsumss  15662  incexclem  15773  prodrblem  15866  fprodcvg  15867  fprodss  15885  fprodn0f  15928  ruclem12  16180  sqrt2irr0  16190  coprmproddvdslem  16603  nnoddn2prmb  16755  prmreclem5  16862  ramub1lem1  16968  mreexd  17579  chnccats1  18562  chnccat  18563  frgpnabllem1  19819  gsumzaddlem  19867  gsum2d  19918  gsumxp2  19926  dmdprdsplitlem  19985  pgpfac1lem2  20023  pgpfac1lem3  20025  irredrmul  20380  lsppratlem3  21121  lbsextlem4  21133  psgnodpmr  21562  frlmsslsp  21768  regsep2  23337  1stckgen  23515  regr1lem  23700  opnsubg  24069  zcld  24775  recld2  24776  bcthlem4  25300  iundisj  25522  iblss2  25780  itgeqa  25788  limcnlp  25852  dvloglem  26630  dvlog2lem  26634  2irrexpq  26713  rtprmirr  26743  logbgcd1irr  26777  ressatans  26917  regamcl  27044  facgam  27049  wilthlem2  27052  2lgslem2  27379  noetasuplem4  27721  noetainflem4  27725  mulsval  28122  tgelrnln  28720  incistruhgr  29170  upgrres1  29404  dfpth2  29820  usgr2pthlem  29854  iundisjf  32682  iundisjfi  32893  gsumfs2d  33161  cycpmfv3  33215  cyc3conja  33257  elrgspnlem4  33345  elrgspnsubrunlem2  33348  mxidlirredi  33570  qsdrngilem  33593  rsprprmprmidlb  33622  rprmirred  33630  rprmirredb  33631  1arithufdlem3  33645  dfufd2  33649  ply1dg3rt0irred  33683  ig1pmindeg  33701  esplyfv  33753  esplyfval3  33755  esplyfvn  33760  fldextrspunlsplem  33857  fldextrspunlsp  33858  submateqlem1  33991  submateqlem2  33992  elzrhunit  34161  qqhval2  34166  esumrnmpt2  34252  inelpisys  34338  plymulx  34732  onint1  36671  lindsadd  37893  lindsenlbs  37895  poimirlem23  37923  poimirlem30  37930  dvasin  37984  areacirclem4  37991  pridlc3  38353  relogbzexpd  42374  dvrelog2b  42465  dvrelogpow2b  42467  aks4d1p1p4  42470  aks4d1p6  42480  aks6d1c7lem1  42579  nelsubginvcld  42895  nelsubgcld  42896  prjspersym  42994  prjspreln0  42996  prjspnvs  43007  rmspecsqrtnq  43292  rmspecnonsq  43293  pr2eldif1  43939  pr2eldif2  43940  disjf1o  45579  difmap  45594  difmapsn  45599  supminfxr2  45856  icoiccdif  45913  iccdificc  45928  climrec  45992  limciccioolb  46010  limcrecl  46018  sumnnodd  46019  lptioo2  46020  lptioo1  46021  limcicciooub  46024  lptre2pt  46027  reclimc  46040  cnrefiisplem  46216  icccncfext  46274  fperdvper  46306  dvnmul  46330  itgcoscmulx  46356  itgsincmulx  46361  stoweidlem34  46421  stoweidlem39  46426  stoweidlem57  46444  wallispi  46457  stirlinglem8  46468  dirkercncflem2  46491  dirkercncflem4  46493  fourierdlem38  46532  fourierdlem40  46534  fourierdlem42  46536  fourierdlem46  46539  fourierdlem53  46546  fourierdlem56  46549  fourierdlem58  46551  fourierdlem62  46555  fourierdlem74  46567  fourierdlem75  46568  fourierdlem76  46569  fourierdlem78  46571  fourierdlem93  46586  fourierdlem103  46596  fourierdlem104  46597  fouriersw  46618  elaa2  46621  etransc  46670  gsumge0cl  46758  sge0fodjrnlem  46803  iundjiun  46847  meadjiunlem  46852  meaiininclem  46873  caragendifcl  46901  caratheodorylem1  46913  hoidmvlelem1  46982  hoidmvlelem2  46983  hoidmvlelem4  46985  hspdifhsp  47003  hspmbllem2  47014  preimagelt  47086  preimalegt  47087  sqrtnegnre  47696  requad01  48010  dig1  48997