Theorem eldifd 3942

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3928

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934

This theorem is referenced by:  rexdifi  4130  eqoreldif  4666  frd  5615  xpdifid  6162  funeldmdif  8052  ressuppssdif  8189  oaf1o  8580  findcard2d  9185  cantnflem1  9708  cantnflem2  9709  ttrcltr  9735  fin23lem26  10344  isf34lem4  10396  isfin7-2  10415  axdc3lem4  10472  axdc4lem  10474  ttukeylem7  10534  pwfseqlem1  10677  pwfseqlem3  10679  hashf1lem1  14478  seqcoll  14487  seqcoll2  14488  rlimcld2  15599  sumrblem  15732  fsumcvg  15733  fsumss  15746  incexclem  15857  prodrblem  15950  fprodcvg  15951  fprodss  15969  fprodn0f  16012  ruclem12  16264  sqrt2irr0  16274  coprmproddvdslem  16686  nnoddn2prmb  16838  prmreclem5  16945  ramub1lem1  17051  mreexd  17659  frgpnabllem1  19859  gsumzaddlem  19907  gsum2d  19958  gsumxp2  19966  dmdprdsplitlem  20025  pgpfac1lem2  20063  pgpfac1lem3  20065  irredrmul  20392  lsppratlem3  21115  lbsextlem4  21127  psgnodpmr  21555  frlmsslsp  21761  regsep2  23319  1stckgen  23497  regr1lem  23682  opnsubg  24051  zcld  24758  recld2  24759  bcthlem4  25284  iundisj  25506  iblss2  25764  itgeqa  25772  limcnlp  25836  dvloglem  26614  dvlog2lem  26618  2irrexpq  26697  rtprmirr  26727  logbgcd1irr  26761  ressatans  26901  regamcl  27028  facgam  27033  wilthlem2  27036  2lgslem2  27363  noetasuplem4  27705  noetainflem4  27709  mulsval  28069  tgelrnln  28614  incistruhgr  29063  upgrres1  29297  dfpth2  29716  usgr2pthlem  29750  iundisjf  32575  iundisjfi  32778  chnccats1  33000  gsumfs2d  33054  cycpmfv3  33131  cyc3conja  33173  elrgspnlem4  33245  elrgspnsubrunlem2  33248  mxidlirredi  33491  qsdrngilem  33514  rsprprmprmidlb  33543  rprmirred  33551  rprmirredb  33552  1arithufdlem3  33566  dfufd2  33570  ply1dg3rt0irred  33600  ig1pmindeg  33616  fldextrspunlsplem  33719  fldextrspunlsp  33720  submateqlem1  33843  submateqlem2  33844  elzrhunit  34013  qqhval2  34018  esumrnmpt2  34104  inelpisys  34190  plymulx  34585  onint1  36472  lindsadd  37642  lindsenlbs  37644  poimirlem23  37672  poimirlem30  37679  dvasin  37733  areacirclem4  37740  pridlc3  38102  relogbzexpd  41993  dvrelog2b  42084  dvrelogpow2b  42086  aks4d1p1p4  42089  aks4d1p6  42099  aks6d1c7lem1  42198  nelsubginvcld  42494  nelsubgcld  42495  prjspersym  42605  prjspreln0  42607  prjspnvs  42618  rmspecsqrtnq  42904  rmspecnonsq  42905  pr2eldif1  43553  pr2eldif2  43554  disjf1o  45195  difmap  45211  difmapsn  45216  supminfxr2  45476  icoiccdif  45533  iccdificc  45548  climrec  45612  limciccioolb  45630  limcrecl  45638  sumnnodd  45639  lptioo2  45640  lptioo1  45641  limcicciooub  45646  lptre2pt  45649  reclimc  45662  cnrefiisplem  45838  icccncfext  45896  fperdvper  45928  dvnmul  45952  itgcoscmulx  45978  itgsincmulx  45983  stoweidlem34  46043  stoweidlem39  46048  stoweidlem57  46066  wallispi  46079  stirlinglem8  46090  dirkercncflem2  46113  dirkercncflem4  46115  fourierdlem38  46154  fourierdlem40  46156  fourierdlem42  46158  fourierdlem46  46161  fourierdlem53  46168  fourierdlem56  46171  fourierdlem58  46173  fourierdlem62  46177  fourierdlem74  46189  fourierdlem75  46190  fourierdlem76  46191  fourierdlem78  46193  fourierdlem93  46208  fourierdlem103  46218  fourierdlem104  46219  fouriersw  46240  elaa2  46243  etransc  46292  gsumge0cl  46380  sge0fodjrnlem  46425  iundjiun  46469  meadjiunlem  46474  meaiininclem  46495  caragendifcl  46523  caratheodorylem1  46535  hoidmvlelem1  46604  hoidmvlelem2  46605  hoidmvlelem4  46607  hspdifhsp  46625  hspmbllem2  46636  preimagelt  46708  preimalegt  46709  sqrtnegnre  47316  requad01  47615  dig1  48568