Theorem eldifd 3917

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2144   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-dif 3909

This theorem is referenced by:  rexdifi  4105  eqoreldif  4646  frd  5606  xpdifid  6155  xpdifcnvepel  6156  funeldmdif  8031  ressuppssdif  8167  oaf1o  8534  findcard2d  9137  cantnflem1  9646  cantnflem2  9647  ttrcltr  9673  fin23lem26  10284  isf34lem4  10336  isfin7-2  10355  axdc3lem4  10412  axdc4lem  10414  ttukeylem7  10474  pwfseqlem1  10618  pwfseqlem3  10620  hashf1lem1  14470  seqcoll  14479  seqcoll2  14480  rlimcld2  15607  sumrblem  15740  fsumcvg  15741  fsumss  15754  incexclem  15868  prodrblem  15961  fprodcvg  15962  fprodss  15980  fprodn0f  16023  ruclem12  16275  sqrt2irr0  16285  coprmproddvdslem  16698  nnoddn2prmb  16851  prmreclem5  16958  ramub1lem1  17064  mreexd  17676  chnccats1  18659  chnccat  18660  frgpnabllem1  19915  gsumzaddlem  19963  gsum2d  20014  gsumxp2  20022  dmdprdsplitlem  20081  pgpfac1lem2  20119  pgpfac1lem3  20121  irredrmul  20478  lsppratlem3  21221  lbsextlem4  21233  psgnodpmr  21644  frlmsslsp  21850  regsep2  23438  1stckgen  23616  regr1lem  23801  opnsubg  24170  zcld  24876  recld2  24877  bcthlem4  25391  iundisj  25612  iblss2  25870  itgeqa  25878  limcnlp  25942  plymulidp  26348  dvloglem  26715  dvlog2lem  26719  2irrexpq  26798  rtprmirr  26827  logbgcd1irr  26861  ressatans  27001  regamcl  27127  facgam  27132  wilthlem2  27135  2lgslem2  27461  noetasuplem4  27802  noetainflem4  27806  mulsval  28204  tgelrnln  28801  tglnpt4  28826  tgelrnpln  28985  lnincplng  28993  plngcplem  28994  plngrotlem1  28996  plngrotlem2  28997  lnssplnglem  29000  lnssplng  29001  incistruhgr  29282  upgrres1  29516  dfpth2  29931  usgr2pthlem  29965  iundisjf  32791  iundisjfi  33000  gsumfs2d  33243  cycpmfv3  33297  cyc3conja  33339  elrgspnlem4  33428  elrgspnsubrunlem2  33431  prmidlsubm  33648  mxidlirredi  33661  qsdrngilem  33684  dflringlem2  33693  dflring3  33695  rsprprmprmidlb  33721  rprmirred  33729  rprmirredb  33730  1arithufdlem3  33744  dfufd2  33748  ply1dg3rt0irred  33782  ig1pmindeg  33800  selvascl  33816  esplyfv  33869  esplyfval3  33871  esplyfvn  33876  fldextrspunlsplem  33972  fldextrspunlsp  33973  submateqlem1  34106  submateqlem2  34107  elzrhunit  34276  qqhval2  34281  esumrnmpt2  34367  inelpisys  34453  nmulprop  36545  onint1  36814  mh-inf3sn  36907  lindsadd  38117  lindsenlbs  38119  poimirlem23  38147  poimirlem30  38154  dvasin  38208  areacirclem4  38215  pridlc3  38577  relogbzexpd  42598  dvrelog2b  42688  dvrelogpow2b  42690  aks4d1p1p4  42693  aks4d1p6  42703  aks6d1c7lem1  42802  nelsubginvcld  43123  nelsubgcld  43124  prjspersym  43194  prjspreln0  43196  prjspnvs  43207  rmspecsqrtnq  43488  rmspecnonsq  43489  pr2eldif1  44135  pr2eldif2  44136  disjf1o  45774  difmap  45788  difmapsn  45793  supminfxr2  46048  icoiccdif  46105  iccdificc  46120  climrec  46184  limciccioolb  46202  limcrecl  46210  sumnnodd  46211  lptioo2  46212  lptioo1  46213  limcicciooub  46216  lptre2pt  46219  reclimc  46232  cnrefiisplem  46408  icccncfext  46466  fperdvper  46498  dvnmul  46522  itgcoscmulx  46548  itgsincmulx  46553  stoweidlem34  46613  stoweidlem39  46618  stoweidlem57  46636  wallispi  46649  stirlinglem8  46660  dirkercncflem2  46683  dirkercncflem4  46685  fourierdlem38  46724  fourierdlem40  46726  fourierdlem42  46728  fourierdlem46  46731  fourierdlem53  46738  fourierdlem56  46741  fourierdlem58  46743  fourierdlem62  46747  fourierdlem74  46759  fourierdlem75  46760  fourierdlem76  46761  fourierdlem78  46763  fourierdlem93  46778  fourierdlem103  46788  fourierdlem104  46789  fouriersw  46810  elaa2  46813  etransc  46862  gsumge0cl  46950  sge0fodjrnlem  46995  iundjiun  47039  meadjiunlem  47044  meaiininclem  47065  caragendifcl  47093  caratheodorylem1  47105  hoidmvlelem1  47174  hoidmvlelem2  47175  hoidmvlelem4  47177  hspdifhsp  47195  hspmbllem2  47206  preimagelt  47278  preimalegt  47279  sqrtnegnre  47906  requad01  48248  dig1  49235