Theorem eldifd 3960

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952

This theorem is referenced by:  rexdifi  4146  eqoreldif  4689  frd  5636  xpdifid  6168  funeldmdif  8034  ressuppssdif  8170  oaf1o  8563  findcard2d  9166  cantnflem1  9684  cantnflem2  9685  ttrcltr  9711  fin23lem26  10320  isf34lem4  10372  isfin7-2  10391  axdc3lem4  10448  axdc4lem  10450  ttukeylem7  10510  pwfseqlem1  10653  pwfseqlem3  10655  hashf1lem1  14415  hashf1lem1OLD  14416  seqcoll  14425  seqcoll2  14426  rlimcld2  15522  sumrblem  15657  fsumcvg  15658  fsumss  15671  incexclem  15782  prodrblem  15873  fprodcvg  15874  fprodss  15892  fprodn0f  15935  ruclem12  16184  sqrt2irr0  16194  coprmproddvdslem  16599  nnoddn2prmb  16746  prmreclem5  16853  ramub1lem1  16959  mreexd  17586  frgpnabllem1  19741  gsumzaddlem  19789  gsum2d  19840  gsumxp2  19848  dmdprdsplitlem  19907  pgpfac1lem2  19945  pgpfac1lem3  19947  irredrmul  20241  lsppratlem3  20762  lbsextlem4  20774  psgnodpmr  21143  frlmsslsp  21351  regsep2  22880  1stckgen  23058  regr1lem  23243  opnsubg  23612  zcld  24329  recld2  24330  bcthlem4  24844  iundisj  25065  iblss2  25323  itgeqa  25331  limcnlp  25395  dvloglem  26156  dvlog2lem  26160  2irrexpq  26239  logbgcd1irr  26299  ressatans  26439  regamcl  26565  facgam  26570  wilthlem2  26573  2lgslem2  26898  noetasuplem4  27239  noetainflem4  27243  mulsval  27568  tgelrnln  27912  incistruhgr  28370  upgrres1  28601  usgr2pthlem  29051  iundisjf  31851  iundisjfi  32038  cycpmfv3  32305  cyc3conja  32347  mxidlirredi  32618  qsdrngilem  32639  ig1pmindeg  32702  submateqlem1  32818  submateqlem2  32819  elzrhunit  32990  qqhval2  32993  esumrnmpt2  33097  inelpisys  33183  plymulx  33590  onint1  35382  lindsadd  36529  lindsenlbs  36531  poimirlem23  36559  poimirlem30  36566  dvasin  36620  areacirclem4  36627  pridlc3  36989  relogbzexpd  40888  dvrelog2b  40979  dvrelogpow2b  40981  aks4d1p1p4  40984  aks4d1p6  40994  nelsubginvcld  41118  nelsubgcld  41119  rtprmirr  41285  prjspersym  41397  prjspreln0  41399  prjspvs  41400  prjspnvs  41410  rmspecsqrtnq  41692  rmspecnonsq  41693  pr2eldif1  42353  pr2eldif2  42354  disjf1o  43937  difmap  43954  difmapsn  43959  supminfxr2  44227  icoiccdif  44285  iccdificc  44300  climrec  44367  limciccioolb  44385  limcrecl  44393  sumnnodd  44394  lptioo2  44395  lptioo1  44396  limcicciooub  44401  lptre2pt  44404  reclimc  44417  cnrefiisplem  44593  icccncfext  44651  fperdvper  44683  dvnmul  44707  itgcoscmulx  44733  itgsincmulx  44738  stoweidlem34  44798  stoweidlem39  44803  stoweidlem57  44821  wallispi  44834  stirlinglem8  44845  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem38  44909  fourierdlem40  44911  fourierdlem42  44913  fourierdlem46  44916  fourierdlem53  44923  fourierdlem56  44926  fourierdlem58  44928  fourierdlem62  44932  fourierdlem74  44944  fourierdlem75  44945  fourierdlem76  44946  fourierdlem78  44948  fourierdlem93  44963  fourierdlem103  44973  fourierdlem104  44974  fouriersw  44995  elaa2  44998  etransc  45047  gsumge0cl  45135  sge0fodjrnlem  45180  iundjiun  45224  meadjiunlem  45229  meaiininclem  45250  caragendifcl  45278  caratheodorylem1  45290  hoidmvlelem1  45359  hoidmvlelem2  45360  hoidmvlelem4  45362  hspdifhsp  45380  hspmbllem2  45391  preimagelt  45463  preimalegt  45464  sqrtnegnre  46063  requad01  46337  dig1  47342