Theorem eldifd 3950

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-dif 3942

This theorem is referenced by:  rexdifi  4125  eqoreldif  4625  xpdifid  6028  funeldmdif  7750  ressuppssdif  7854  oaf1o  8192  findcard2d  8763  cantnflem1  9155  cantnflem2  9156  fin23lem26  9750  isf34lem4  9802  isfin7-2  9821  axdc3lem4  9878  axdc4lem  9880  ttukeylem7  9940  pwfseqlem1  10083  pwfseqlem3  10085  hashf1lem1  13816  seqcoll  13825  seqcoll2  13826  rlimcld2  14938  sumrblem  15071  fsumcvg  15072  fsumss  15085  incexclem  15194  prodrblem  15286  fprodcvg  15287  fprodss  15305  fprodn0f  15348  ruclem12  15597  sqrt2irr0  15607  coprmproddvdslem  16009  nnoddn2prmb  16153  prmreclem5  16259  ramub1lem1  16365  mreexd  16916  frgpnabllem1  18996  gsumzaddlem  19044  gsum2d  19095  gsumxp2  19103  dmdprdsplitlem  19162  pgpfac1lem2  19200  pgpfac1lem3  19202  irredrmul  19460  lsppratlem3  19924  lbsextlem4  19936  psgnodpmr  20737  frlmsslsp  20943  regsep2  21987  1stckgen  22165  regr1lem  22350  opnsubg  22719  zcld  23424  recld2  23425  bcthlem4  23933  iundisj  24152  iblss2  24409  itgeqa  24417  limcnlp  24479  dvloglem  25234  dvlog2lem  25238  2irrexpq  25316  logbgcd1irr  25375  ressatans  25515  regamcl  25641  facgam  25646  wilthlem2  25649  2lgslem2  25974  tgelrnln  26419  incistruhgr  26867  upgrres1  27098  usgr2pthlem  27547  iundisjf  30342  iundisjfi  30522  cycpmfv3  30761  cyc3conja  30803  submateqlem1  31076  submateqlem2  31077  elzrhunit  31224  qqhval2  31227  esumrnmpt2  31331  inelpisys  31417  plymulx  31822  noetalem3  33223  onint1  33801  lindsadd  34889  lindsenlbs  34891  poimirlem23  34919  poimirlem30  34926  dvasin  34982  areacirclem4  34989  pridlc3  35355  nelsubginvcld  39134  nelsubgcld  39135  rtprmirr  39200  prjspersym  39263  prjspreln0  39265  prjspvs  39266  rmspecsqrtnq  39509  rmspecnonsq  39510  pr2eldif1  39919  pr2eldif2  39920  disjf1o  41458  difmap  41476  difmapsn  41481  supminfxr2  41751  icoiccdif  41806  iccdificc  41821  climrec  41890  limciccioolb  41908  limcrecl  41916  sumnnodd  41917  lptioo2  41918  lptioo1  41919  limcicciooub  41924  lptre2pt  41927  reclimc  41940  cnrefiisplem  42116  icccncfext  42176  fperdvper  42209  dvnmul  42234  itgcoscmulx  42260  itgsincmulx  42265  stoweidlem34  42326  stoweidlem39  42331  stoweidlem57  42349  wallispi  42362  stirlinglem8  42373  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem38  42437  fourierdlem40  42439  fourierdlem42  42441  fourierdlem46  42444  fourierdlem53  42451  fourierdlem56  42454  fourierdlem58  42456  fourierdlem62  42460  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem78  42476  fourierdlem93  42491  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  elaa2  42526  etransc  42575  gsumge0cl  42660  sge0fodjrnlem  42705  iundjiun  42749  meadjiunlem  42754  meaiininclem  42775  caragendifcl  42803  caratheodorylem1  42815  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem4  42887  hspdifhsp  42905  hspmbllem2  42916  preimagelt  42987  preimalegt  42988  sqrtnegnre  43514  requad01  43793  dig1  44675