Theorem eldifd 3925

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917

This theorem is referenced by:  rexdifi  4113  eqoreldif  4649  frd  5595  xpdifid  6141  funeldmdif  8027  ressuppssdif  8164  oaf1o  8527  findcard2d  9130  cantnflem1  9642  cantnflem2  9643  ttrcltr  9669  fin23lem26  10278  isf34lem4  10330  isfin7-2  10349  axdc3lem4  10406  axdc4lem  10408  ttukeylem7  10468  pwfseqlem1  10611  pwfseqlem3  10613  hashf1lem1  14420  seqcoll  14429  seqcoll2  14430  rlimcld2  15544  sumrblem  15677  fsumcvg  15678  fsumss  15691  incexclem  15802  prodrblem  15895  fprodcvg  15896  fprodss  15914  fprodn0f  15957  ruclem12  16209  sqrt2irr0  16219  coprmproddvdslem  16632  nnoddn2prmb  16784  prmreclem5  16891  ramub1lem1  16997  mreexd  17603  frgpnabllem1  19803  gsumzaddlem  19851  gsum2d  19902  gsumxp2  19910  dmdprdsplitlem  19969  pgpfac1lem2  20007  pgpfac1lem3  20009  irredrmul  20336  lsppratlem3  21059  lbsextlem4  21071  psgnodpmr  21499  frlmsslsp  21705  regsep2  23263  1stckgen  23441  regr1lem  23626  opnsubg  23995  zcld  24702  recld2  24703  bcthlem4  25227  iundisj  25449  iblss2  25707  itgeqa  25715  limcnlp  25779  dvloglem  26557  dvlog2lem  26561  2irrexpq  26640  rtprmirr  26670  logbgcd1irr  26704  ressatans  26844  regamcl  26971  facgam  26976  wilthlem2  26979  2lgslem2  27306  noetasuplem4  27648  noetainflem4  27652  mulsval  28012  tgelrnln  28557  incistruhgr  29006  upgrres1  29240  dfpth2  29659  usgr2pthlem  29693  iundisjf  32518  iundisjfi  32719  chnccats1  32941  gsumfs2d  32995  cycpmfv3  33072  cyc3conja  33114  elrgspnlem4  33196  elrgspnsubrunlem2  33199  mxidlirredi  33442  qsdrngilem  33465  rsprprmprmidlb  33494  rprmirred  33502  rprmirredb  33503  1arithufdlem3  33517  dfufd2  33521  ply1dg3rt0irred  33551  ig1pmindeg  33567  fldextrspunlsplem  33668  fldextrspunlsp  33669  submateqlem1  33797  submateqlem2  33798  elzrhunit  33967  qqhval2  33972  esumrnmpt2  34058  inelpisys  34144  plymulx  34539  onint1  36437  lindsadd  37607  lindsenlbs  37609  poimirlem23  37637  poimirlem30  37644  dvasin  37698  areacirclem4  37705  pridlc3  38067  relogbzexpd  41963  dvrelog2b  42054  dvrelogpow2b  42056  aks4d1p1p4  42059  aks4d1p6  42069  aks6d1c7lem1  42168  nelsubginvcld  42484  nelsubgcld  42485  prjspersym  42595  prjspreln0  42597  prjspnvs  42608  rmspecsqrtnq  42894  rmspecnonsq  42895  pr2eldif1  43543  pr2eldif2  43544  disjf1o  45185  difmap  45201  difmapsn  45206  supminfxr2  45465  icoiccdif  45522  iccdificc  45537  climrec  45601  limciccioolb  45619  limcrecl  45627  sumnnodd  45628  lptioo2  45629  lptioo1  45630  limcicciooub  45635  lptre2pt  45638  reclimc  45651  cnrefiisplem  45827  icccncfext  45885  fperdvper  45917  dvnmul  45941  itgcoscmulx  45967  itgsincmulx  45972  stoweidlem34  46032  stoweidlem39  46037  stoweidlem57  46055  wallispi  46068  stirlinglem8  46079  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem38  46143  fourierdlem40  46145  fourierdlem42  46147  fourierdlem46  46150  fourierdlem53  46157  fourierdlem56  46160  fourierdlem58  46162  fourierdlem62  46166  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  elaa2  46232  etransc  46281  gsumge0cl  46369  sge0fodjrnlem  46414  iundjiun  46458  meadjiunlem  46463  meaiininclem  46484  caragendifcl  46512  caratheodorylem1  46524  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem4  46596  hspdifhsp  46614  hspmbllem2  46625  preimagelt  46697  preimalegt  46698  sqrtnegnre  47305  requad01  47619  dig1  48594