Theorem eldifd 3910

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902

This theorem is used by:  rexdifi  4097  eqoreldif  4646  frd  5608  xpdifid  6159  xpdifcnvepel  6160  funeldmdif  8059  ressuppssdif  8202  oaf1o  8571  findcard2d  9182  cantnflem1  9690  cantnflem2  9691  ttrcltr  9717  fin23lem26  10403  isf34lem4  10455  isfin7-2  10474  axdc3lem4  10531  axdc4lem  10533  ttukeylem7  10593  pwfseqlem1  10743  pwfseqlem3  10745  hashf1lem1  14600  seqcoll  14609  seqcoll2  14610  rlimcld2  15745  sumrblem  15877  fsumcvg  15878  fsumss  15891  incexclem  16005  prodrblem  16096  fprodcvg  16097  fprodss  16115  fprodn0f  16158  ruclem12  16409  sqrt2irr0  16419  coprmproddvdslem  16837  nnoddn2prmb  16991  prmreclem5  17098  ramub1lem1  17204  mreexd  17816  chnccats1  18799  chnccat  18800  frgpnabllem1  20087  gsumzaddlem  20135  gsum2d  20186  gsumxp2  20194  dmdprdsplitlem  20253  pgpfac1lem2  20291  pgpfac1lem3  20293  irredrmul  20657  lsppratlem3  21427  lbsextlem4  21439  cmprmidlmcl  21631  prmidlsubm  21643  psgnodpmr  21896  frlmsslsp  22102  lindsenlbs  22157  regsep2  23694  1stckgen  23873  regr1lem  24058  opnsubg  24427  zcld  25133  recld2  25134  bcthlem4  25648  iundisj  25869  iblss2  26126  itgeqa  26134  limcnlp  26198  plymulidp  26603  dvloglem  26976  dvlog2lem  26980  2irrexpq  27059  rtprmirr  27088  logbgcd1irr  27122  ressatans  27262  regamcl  27388  facgam  27393  wilthlem2  27396  2lgslem2  27722  noetasuplem4  28093  noetainflem4  28097  mulsval  28495  tgelrnln  29098  tglnpt4  29123  tgelrnpln  29254  lnincplng  29262  plngcplem  29263  plngrotlem1  29265  plngrotlem2  29266  lnssplnglem  29269  lnssplng  29270  nhpmirhp  29276  perpeq  29348  tgaaddcpbllem1  29349  tgaaddcpbl  29352  tgaaddcpbl2  29353  prlnghpg  29424  dfprlng2  29425  prlngpln3  29427  prlngex  29429  prlngmolem2  29431  prlngmo2  29434  prlngpln4  29436  symquadprlng  29440  prlngsymquadlem  29441  quadcgrprlng  29444  incistruhgr  29657  upgrres1  29894  dfpth2  30314  usgr2pthlem  30349  iundisjf  33183  iundisjfi  33388  gsumfs2d  33622  cycpmfv3  33676  cyc3conja  33718  elrgspnlem4  33806  elrgspnsubrunlem2  33809  mxidlirredi  33996  qsdrngilem  34018  dflringlem2  34027  dflring3  34029  rsprprmprmidlb  34055  rprmirred  34063  rprmirredb  34064  1arithufdlem3  34078  dfufd2  34082  ply1dg3rt0irred  34116  ig1pmindeg  34134  selvascl  34149  esplyfv  34202  esplyfval3  34204  esplyfvn  34209  fldextrspunlsplem  34305  fldextrspunlsp  34306  submateqlem1  34439  submateqlem2  34440  elzrhunit  34609  qqhval2  34614  esumrnmpt2  34700  inelpisys  34787  nmulprop  36939  onint1  37237  mh-inf3sn  37330  lindsadd  38536  poimirlem23  38561  poimirlem30  38568  dvasin  38622  areacirclem4  38629  pridlc3  39007  relogbzexpd  43026  dvrelog2b  43116  dvrelogpow2b  43118  aks4d1p1p4  43121  aks4d1p6  43131  aks6d1c7lem1  43230  nelsubginvcld  43560  nelsubgcld  43561  prjspersym  43635  prjspreln0  43637  prjspnvs  43648  rmspecsqrtnq  43912  rmspecnonsq  43913  pr2eldif1  44554  pr2eldif2  44555  disjf1o  46205  difmap  46219  difmapsn  46224  supminfxr2  46478  icoiccdif  46535  iccdificc  46550  climrec  46614  limciccioolb  46632  limcrecl  46640  sumnnodd  46641  lptioo2  46642  lptioo1  46643  limcicciooub  46646  lptre2pt  46649  reclimc  46662  cnrefiisplem  46838  icccncfext  46896  fperdvper  46928  dvnmul  46952  itgcoscmulx  46978  itgsincmulx  46983  stoweidlem34  47043  stoweidlem39  47048  stoweidlem57  47066  wallispi  47079  stirlinglem8  47090  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem38  47154  fourierdlem40  47156  fourierdlem42  47158  fourierdlem46  47161  fourierdlem53  47168  fourierdlem56  47171  fourierdlem58  47173  fourierdlem62  47177  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem78  47193  fourierdlem93  47208  fourierdlem103  47218  fourierdlem104  47219  fouriersw  47240  elaa2  47243  etransc  47292  gsumge0cl  47380  sge0fodjrnlem  47425  iundjiun  47469  meadjiunlem  47474  meaiininclem  47495  caragendifcl  47523  caratheodorylem1  47535  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem4  47607  hspdifhsp  47625  hspmbllem2  47636  preimagelt  47708  preimalegt  47709  sqrtnegnre  48376  requad01  48718  dig1  49719