Theorem eldifd 3961

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953

This theorem is referenced by:  rexdifi  4149  eqoreldif  4684  frd  5640  xpdifid  6187  funeldmdif  8074  ressuppssdif  8211  oaf1o  8602  findcard2d  9207  cantnflem1  9730  cantnflem2  9731  ttrcltr  9757  fin23lem26  10366  isf34lem4  10418  isfin7-2  10437  axdc3lem4  10494  axdc4lem  10496  ttukeylem7  10556  pwfseqlem1  10699  pwfseqlem3  10701  hashf1lem1  14495  seqcoll  14504  seqcoll2  14505  rlimcld2  15615  sumrblem  15748  fsumcvg  15749  fsumss  15762  incexclem  15873  prodrblem  15966  fprodcvg  15967  fprodss  15985  fprodn0f  16028  ruclem12  16278  sqrt2irr0  16288  coprmproddvdslem  16700  nnoddn2prmb  16852  prmreclem5  16959  ramub1lem1  17065  mreexd  17686  frgpnabllem1  19892  gsumzaddlem  19940  gsum2d  19991  gsumxp2  19999  dmdprdsplitlem  20058  pgpfac1lem2  20096  pgpfac1lem3  20098  irredrmul  20428  lsppratlem3  21152  lbsextlem4  21164  psgnodpmr  21609  frlmsslsp  21817  regsep2  23385  1stckgen  23563  regr1lem  23748  opnsubg  24117  zcld  24836  recld2  24837  bcthlem4  25362  iundisj  25584  iblss2  25842  itgeqa  25850  limcnlp  25914  dvloglem  26691  dvlog2lem  26695  2irrexpq  26774  rtprmirr  26804  logbgcd1irr  26838  ressatans  26978  regamcl  27105  facgam  27110  wilthlem2  27113  2lgslem2  27440  noetasuplem4  27782  noetainflem4  27786  mulsval  28136  tgelrnln  28639  incistruhgr  29097  upgrres1  29331  dfpth2  29750  usgr2pthlem  29784  iundisjf  32603  iundisjfi  32799  chnccats1  33006  gsumfs2d  33059  cycpmfv3  33136  cyc3conja  33178  elrgspnlem4  33250  elrgspnsubrunlem2  33253  mxidlirredi  33500  qsdrngilem  33523  rsprprmprmidlb  33552  rprmirred  33560  rprmirredb  33561  1arithufdlem3  33575  dfufd2  33579  ply1dg3rt0irred  33608  ig1pmindeg  33623  fldextrspunlsplem  33724  fldextrspunlsp  33725  submateqlem1  33807  submateqlem2  33808  elzrhunit  33979  qqhval2  33984  esumrnmpt2  34070  inelpisys  34156  plymulx  34564  onint1  36451  lindsadd  37621  lindsenlbs  37623  poimirlem23  37651  poimirlem30  37658  dvasin  37712  areacirclem4  37719  pridlc3  38081  relogbzexpd  41977  dvrelog2b  42068  dvrelogpow2b  42070  aks4d1p1p4  42073  aks4d1p6  42083  aks6d1c7lem1  42182  nelsubginvcld  42511  nelsubgcld  42512  prjspersym  42622  prjspreln0  42624  prjspnvs  42635  rmspecsqrtnq  42922  rmspecnonsq  42923  pr2eldif1  43572  pr2eldif2  43573  disjf1o  45201  difmap  45217  difmapsn  45222  supminfxr2  45485  icoiccdif  45542  iccdificc  45557  climrec  45623  limciccioolb  45641  limcrecl  45649  sumnnodd  45650  lptioo2  45651  lptioo1  45652  limcicciooub  45657  lptre2pt  45660  reclimc  45673  cnrefiisplem  45849  icccncfext  45907  fperdvper  45939  dvnmul  45963  itgcoscmulx  45989  itgsincmulx  45994  stoweidlem34  46054  stoweidlem39  46059  stoweidlem57  46077  wallispi  46090  stirlinglem8  46101  dirkercncflem2  46124  dirkercncflem4  46126  fourierdlem38  46165  fourierdlem40  46167  fourierdlem42  46169  fourierdlem46  46172  fourierdlem53  46179  fourierdlem56  46182  fourierdlem58  46184  fourierdlem62  46188  fourierdlem74  46200  fourierdlem75  46201  fourierdlem76  46202  fourierdlem78  46204  fourierdlem93  46219  fourierdlem103  46229  fourierdlem104  46230  fouriersw  46251  elaa2  46254  etransc  46303  gsumge0cl  46391  sge0fodjrnlem  46436  iundjiun  46480  meadjiunlem  46485  meaiininclem  46506  caragendifcl  46534  caratheodorylem1  46546  hoidmvlelem1  46615  hoidmvlelem2  46616  hoidmvlelem4  46618  hspdifhsp  46636  hspmbllem2  46647  preimagelt  46719  preimalegt  46720  sqrtnegnre  47324  requad01  47613  dig1  48534