Theorem eldifd 3959

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   ∖ cdif 3945

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951

This theorem is referenced by:  rexdifi  4145  eqoreldif  4688  frd  5635  xpdifid  6167  funeldmdif  8033  ressuppssdif  8169  oaf1o  8562  findcard2d  9165  cantnflem1  9683  cantnflem2  9684  ttrcltr  9710  fin23lem26  10319  isf34lem4  10371  isfin7-2  10390  axdc3lem4  10447  axdc4lem  10449  ttukeylem7  10509  pwfseqlem1  10652  pwfseqlem3  10654  hashf1lem1  14414  hashf1lem1OLD  14415  seqcoll  14424  seqcoll2  14425  rlimcld2  15521  sumrblem  15656  fsumcvg  15657  fsumss  15670  incexclem  15781  prodrblem  15872  fprodcvg  15873  fprodss  15891  fprodn0f  15934  ruclem12  16183  sqrt2irr0  16193  coprmproddvdslem  16598  nnoddn2prmb  16745  prmreclem5  16852  ramub1lem1  16958  mreexd  17585  frgpnabllem1  19740  gsumzaddlem  19788  gsum2d  19839  gsumxp2  19847  dmdprdsplitlem  19906  pgpfac1lem2  19944  pgpfac1lem3  19946  irredrmul  20240  lsppratlem3  20761  lbsextlem4  20773  psgnodpmr  21142  frlmsslsp  21350  regsep2  22879  1stckgen  23057  regr1lem  23242  opnsubg  23611  zcld  24328  recld2  24329  bcthlem4  24843  iundisj  25064  iblss2  25322  itgeqa  25330  limcnlp  25394  dvloglem  26155  dvlog2lem  26159  2irrexpq  26237  logbgcd1irr  26296  ressatans  26436  regamcl  26562  facgam  26567  wilthlem2  26570  2lgslem2  26895  noetasuplem4  27236  noetainflem4  27240  mulsval  27562  tgelrnln  27878  incistruhgr  28336  upgrres1  28567  usgr2pthlem  29017  iundisjf  31815  iundisjfi  32002  cycpmfv3  32269  cyc3conja  32311  mxidlirredi  32582  qsdrngilem  32603  ig1pmindeg  32666  submateqlem1  32782  submateqlem2  32783  elzrhunit  32954  qqhval2  32957  esumrnmpt2  33061  inelpisys  33147  plymulx  33554  onint1  35329  lindsadd  36476  lindsenlbs  36478  poimirlem23  36506  poimirlem30  36513  dvasin  36567  areacirclem4  36574  pridlc3  36936  relogbzexpd  40835  dvrelog2b  40926  dvrelogpow2b  40928  aks4d1p1p4  40931  aks4d1p6  40941  nelsubginvcld  41072  nelsubgcld  41073  rtprmirr  41238  prjspersym  41350  prjspreln0  41352  prjspvs  41353  prjspnvs  41363  rmspecsqrtnq  41634  rmspecnonsq  41635  pr2eldif1  42295  pr2eldif2  42296  disjf1o  43879  difmap  43896  difmapsn  43901  supminfxr2  44169  icoiccdif  44227  iccdificc  44242  climrec  44309  limciccioolb  44327  limcrecl  44335  sumnnodd  44336  lptioo2  44337  lptioo1  44338  limcicciooub  44343  lptre2pt  44346  reclimc  44359  cnrefiisplem  44535  icccncfext  44593  fperdvper  44625  dvnmul  44649  itgcoscmulx  44675  itgsincmulx  44680  stoweidlem34  44740  stoweidlem39  44745  stoweidlem57  44763  wallispi  44776  stirlinglem8  44787  dirkercncflem2  44810  dirkercncflem4  44812  fourierdlem38  44851  fourierdlem40  44853  fourierdlem42  44855  fourierdlem46  44858  fourierdlem53  44865  fourierdlem56  44868  fourierdlem58  44870  fourierdlem62  44874  fourierdlem74  44886  fourierdlem75  44887  fourierdlem76  44888  fourierdlem78  44890  fourierdlem93  44905  fourierdlem103  44915  fourierdlem104  44916  fouriersw  44937  elaa2  44940  etransc  44989  gsumge0cl  45077  sge0fodjrnlem  45122  iundjiun  45166  meadjiunlem  45171  meaiininclem  45192  caragendifcl  45220  caratheodorylem1  45232  hoidmvlelem1  45301  hoidmvlelem2  45302  hoidmvlelem4  45304  hspdifhsp  45322  hspmbllem2  45333  preimagelt  45405  preimalegt  45406  sqrtnegnre  46005  requad01  46279  dig1  47284