Theorem eldifd 3935

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

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

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3488  df-dif 3927

This theorem is referenced by:  rexdifi  4110  eqoreldif  4608  xpdifid  6011  funeldmdif  7733  ressuppssdif  7837  oaf1o  8175  findcard2d  8746  cantnflem1  9138  cantnflem2  9139  fin23lem26  9733  isf34lem4  9785  isfin7-2  9804  axdc3lem4  9861  axdc4lem  9863  ttukeylem7  9923  pwfseqlem1  10066  pwfseqlem3  10068  hashf1lem1  13803  seqcoll  13812  seqcoll2  13813  rlimcld2  14920  sumrblem  15053  fsumcvg  15054  fsumss  15067  incexclem  15176  prodrblem  15268  fprodcvg  15269  fprodss  15287  fprodn0f  15330  ruclem12  15579  sqrt2irr0  15589  coprmproddvdslem  15989  nnoddn2prmb  16133  prmreclem5  16239  ramub1lem1  16345  mreexd  16896  frgpnabllem1  18976  gsumzaddlem  19024  gsum2d  19075  gsumxp2  19083  dmdprdsplitlem  19142  pgpfac1lem2  19180  pgpfac1lem3  19182  irredrmul  19440  lsppratlem3  19904  lbsextlem4  19916  psgnodpmr  20717  frlmsslsp  20923  regsep2  21967  1stckgen  22145  regr1lem  22330  opnsubg  22699  zcld  23404  recld2  23405  bcthlem4  23913  iundisj  24132  iblss2  24389  itgeqa  24397  limcnlp  24461  dvloglem  25217  dvlog2lem  25221  2irrexpq  25299  logbgcd1irr  25358  ressatans  25498  regamcl  25624  facgam  25629  wilthlem2  25632  2lgslem2  25957  tgelrnln  26402  incistruhgr  26850  upgrres1  27081  usgr2pthlem  27530  iundisjf  30325  iundisjfi  30505  cycpmfv3  30764  cyc3conja  30806  submateqlem1  31082  submateqlem2  31083  elzrhunit  31227  qqhval2  31230  esumrnmpt2  31334  inelpisys  31420  plymulx  31825  noetalem3  33226  onint1  33804  lindsadd  34919  lindsenlbs  34921  poimirlem23  34949  poimirlem30  34956  dvasin  35010  areacirclem4  35017  pridlc3  35383  nelsubginvcld  39203  nelsubgcld  39204  rtprmirr  39269  prjspersym  39349  prjspreln0  39351  prjspvs  39352  rmspecsqrtnq  39595  rmspecnonsq  39596  pr2eldif1  40003  pr2eldif2  40004  disjf1o  41542  difmap  41560  difmapsn  41565  supminfxr2  41835  icoiccdif  41890  iccdificc  41905  climrec  41974  limciccioolb  41992  limcrecl  42000  sumnnodd  42001  lptioo2  42002  lptioo1  42003  limcicciooub  42008  lptre2pt  42011  reclimc  42024  cnrefiisplem  42200  icccncfext  42260  fperdvper  42293  dvnmul  42318  itgcoscmulx  42344  itgsincmulx  42349  stoweidlem34  42409  stoweidlem39  42414  stoweidlem57  42432  wallispi  42445  stirlinglem8  42456  dirkercncflem2  42479  dirkercncflem4  42481  fourierdlem38  42520  fourierdlem40  42522  fourierdlem42  42524  fourierdlem46  42527  fourierdlem53  42534  fourierdlem56  42537  fourierdlem58  42539  fourierdlem62  42543  fourierdlem74  42555  fourierdlem75  42556  fourierdlem76  42557  fourierdlem78  42559  fourierdlem93  42574  fourierdlem103  42584  fourierdlem104  42585  fouriersw  42606  elaa2  42609  etransc  42658  gsumge0cl  42743  sge0fodjrnlem  42788  iundjiun  42832  meadjiunlem  42837  meaiininclem  42858  caragendifcl  42886  caratheodorylem1  42898  hoidmvlelem1  42967  hoidmvlelem2  42968  hoidmvlelem4  42970  hspdifhsp  42988  hspmbllem2  42999  preimagelt  43070  preimalegt  43071  sqrtnegnre  43597  requad01  43871  dig1  44753