Theorem eldifd 3908

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900

This theorem is referenced by:  rexdifi  4097  eqoreldif  4635  frd  5571  xpdifid  6115  funeldmdif  7980  ressuppssdif  8115  oaf1o  8478  findcard2d  9076  cantnflem1  9579  cantnflem2  9580  ttrcltr  9606  fin23lem26  10216  isf34lem4  10268  isfin7-2  10287  axdc3lem4  10344  axdc4lem  10346  ttukeylem7  10406  pwfseqlem1  10549  pwfseqlem3  10551  hashf1lem1  14362  seqcoll  14371  seqcoll2  14372  rlimcld2  15485  sumrblem  15618  fsumcvg  15619  fsumss  15632  incexclem  15743  prodrblem  15836  fprodcvg  15837  fprodss  15855  fprodn0f  15898  ruclem12  16150  sqrt2irr0  16160  coprmproddvdslem  16573  nnoddn2prmb  16725  prmreclem5  16832  ramub1lem1  16938  mreexd  17548  chnccats1  18531  chnccat  18532  frgpnabllem1  19785  gsumzaddlem  19833  gsum2d  19884  gsumxp2  19892  dmdprdsplitlem  19951  pgpfac1lem2  19989  pgpfac1lem3  19991  irredrmul  20345  lsppratlem3  21086  lbsextlem4  21098  psgnodpmr  21527  frlmsslsp  21733  regsep2  23291  1stckgen  23469  regr1lem  23654  opnsubg  24023  zcld  24729  recld2  24730  bcthlem4  25254  iundisj  25476  iblss2  25734  itgeqa  25742  limcnlp  25806  dvloglem  26584  dvlog2lem  26588  2irrexpq  26667  rtprmirr  26697  logbgcd1irr  26731  ressatans  26871  regamcl  26998  facgam  27003  wilthlem2  27006  2lgslem2  27333  noetasuplem4  27675  noetainflem4  27679  mulsval  28048  tgelrnln  28608  incistruhgr  29057  upgrres1  29291  dfpth2  29707  usgr2pthlem  29741  iundisjf  32569  iundisjfi  32778  gsumfs2d  33035  cycpmfv3  33084  cyc3conja  33126  elrgspnlem4  33212  elrgspnsubrunlem2  33215  mxidlirredi  33436  qsdrngilem  33459  rsprprmprmidlb  33488  rprmirred  33496  rprmirredb  33497  1arithufdlem3  33511  dfufd2  33515  ply1dg3rt0irred  33546  ig1pmindeg  33562  esplyfv  33591  fldextrspunlsplem  33686  fldextrspunlsp  33687  submateqlem1  33820  submateqlem2  33821  elzrhunit  33990  qqhval2  33995  esumrnmpt2  34081  inelpisys  34167  plymulx  34561  onint1  36493  lindsadd  37652  lindsenlbs  37654  poimirlem23  37682  poimirlem30  37689  dvasin  37743  areacirclem4  37750  pridlc3  38112  relogbzexpd  42067  dvrelog2b  42158  dvrelogpow2b  42160  aks4d1p1p4  42163  aks4d1p6  42173  aks6d1c7lem1  42272  nelsubginvcld  42588  nelsubgcld  42589  prjspersym  42699  prjspreln0  42701  prjspnvs  42712  rmspecsqrtnq  42998  rmspecnonsq  42999  pr2eldif1  43646  pr2eldif2  43647  disjf1o  45287  difmap  45303  difmapsn  45308  supminfxr2  45566  icoiccdif  45623  iccdificc  45638  climrec  45702  limciccioolb  45720  limcrecl  45728  sumnnodd  45729  lptioo2  45730  lptioo1  45731  limcicciooub  45734  lptre2pt  45737  reclimc  45750  cnrefiisplem  45926  icccncfext  45984  fperdvper  46016  dvnmul  46040  itgcoscmulx  46066  itgsincmulx  46071  stoweidlem34  46131  stoweidlem39  46136  stoweidlem57  46154  wallispi  46167  stirlinglem8  46178  dirkercncflem2  46201  dirkercncflem4  46203  fourierdlem38  46242  fourierdlem40  46244  fourierdlem42  46246  fourierdlem46  46249  fourierdlem53  46256  fourierdlem56  46259  fourierdlem58  46261  fourierdlem62  46265  fourierdlem74  46277  fourierdlem75  46278  fourierdlem76  46279  fourierdlem78  46281  fourierdlem93  46296  fourierdlem103  46306  fourierdlem104  46307  fouriersw  46328  elaa2  46331  etransc  46380  gsumge0cl  46468  sge0fodjrnlem  46513  iundjiun  46557  meadjiunlem  46562  meaiininclem  46583  caragendifcl  46611  caratheodorylem1  46623  hoidmvlelem1  46692  hoidmvlelem2  46693  hoidmvlelem4  46695  hspdifhsp  46713  hspmbllem2  46724  preimagelt  46796  preimalegt  46797  sqrtnegnre  47406  requad01  47720  dig1  48708