Theorem eldifd 3910

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ∖ cdif 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902

This theorem is referenced by:  rexdifi  4100  eqoreldif  4640  frd  5579  xpdifid  6124  funeldmdif  7990  ressuppssdif  8125  oaf1o  8488  findcard2d  9089  cantnflem1  9596  cantnflem2  9597  ttrcltr  9623  fin23lem26  10233  isf34lem4  10285  isfin7-2  10304  axdc3lem4  10361  axdc4lem  10363  ttukeylem7  10423  pwfseqlem1  10567  pwfseqlem3  10569  hashf1lem1  14376  seqcoll  14385  seqcoll2  14386  rlimcld2  15499  sumrblem  15632  fsumcvg  15633  fsumss  15646  incexclem  15757  prodrblem  15850  fprodcvg  15851  fprodss  15869  fprodn0f  15912  ruclem12  16164  sqrt2irr0  16174  coprmproddvdslem  16587  nnoddn2prmb  16739  prmreclem5  16846  ramub1lem1  16952  mreexd  17563  chnccats1  18546  chnccat  18547  frgpnabllem1  19800  gsumzaddlem  19848  gsum2d  19899  gsumxp2  19907  dmdprdsplitlem  19966  pgpfac1lem2  20004  pgpfac1lem3  20006  irredrmul  20361  lsppratlem3  21102  lbsextlem4  21114  psgnodpmr  21543  frlmsslsp  21749  regsep2  23318  1stckgen  23496  regr1lem  23681  opnsubg  24050  zcld  24756  recld2  24757  bcthlem4  25281  iundisj  25503  iblss2  25761  itgeqa  25769  limcnlp  25833  dvloglem  26611  dvlog2lem  26615  2irrexpq  26694  rtprmirr  26724  logbgcd1irr  26758  ressatans  26898  regamcl  27025  facgam  27030  wilthlem2  27033  2lgslem2  27360  noetasuplem4  27702  noetainflem4  27706  mulsval  28078  tgelrnln  28651  incistruhgr  29101  upgrres1  29335  dfpth2  29751  usgr2pthlem  29785  iundisjf  32613  iundisjfi  32825  gsumfs2d  33093  cycpmfv3  33146  cyc3conja  33188  elrgspnlem4  33276  elrgspnsubrunlem2  33279  mxidlirredi  33501  qsdrngilem  33524  rsprprmprmidlb  33553  rprmirred  33561  rprmirredb  33562  1arithufdlem3  33576  dfufd2  33580  ply1dg3rt0irred  33614  ig1pmindeg  33632  esplyfv  33677  esplyfval3  33679  esplyfvn  33682  fldextrspunlsplem  33779  fldextrspunlsp  33780  submateqlem1  33913  submateqlem2  33914  elzrhunit  34083  qqhval2  34088  esumrnmpt2  34174  inelpisys  34260  plymulx  34654  onint1  36592  lindsadd  37753  lindsenlbs  37755  poimirlem23  37783  poimirlem30  37790  dvasin  37844  areacirclem4  37851  pridlc3  38213  relogbzexpd  42168  dvrelog2b  42259  dvrelogpow2b  42261  aks4d1p1p4  42264  aks4d1p6  42274  aks6d1c7lem1  42373  nelsubginvcld  42693  nelsubgcld  42694  prjspersym  42792  prjspreln0  42794  prjspnvs  42805  rmspecsqrtnq  43090  rmspecnonsq  43091  pr2eldif1  43737  pr2eldif2  43738  disjf1o  45377  difmap  45393  difmapsn  45398  supminfxr2  45655  icoiccdif  45712  iccdificc  45727  climrec  45791  limciccioolb  45809  limcrecl  45817  sumnnodd  45818  lptioo2  45819  lptioo1  45820  limcicciooub  45823  lptre2pt  45826  reclimc  45839  cnrefiisplem  46015  icccncfext  46073  fperdvper  46105  dvnmul  46129  itgcoscmulx  46155  itgsincmulx  46160  stoweidlem34  46220  stoweidlem39  46225  stoweidlem57  46243  wallispi  46256  stirlinglem8  46267  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem38  46331  fourierdlem40  46333  fourierdlem42  46335  fourierdlem46  46338  fourierdlem53  46345  fourierdlem56  46348  fourierdlem58  46350  fourierdlem62  46354  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem93  46385  fourierdlem103  46395  fourierdlem104  46396  fouriersw  46417  elaa2  46420  etransc  46469  gsumge0cl  46557  sge0fodjrnlem  46602  iundjiun  46646  meadjiunlem  46651  meaiininclem  46672  caragendifcl  46700  caratheodorylem1  46712  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem4  46784  hspdifhsp  46802  hspmbllem2  46813  preimagelt  46885  preimalegt  46886  sqrtnegnre  47495  requad01  47809  dig1  48796