Theorem eldifd 3894

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886

This theorem is referenced by:  rexdifi  4076  eqoreldif  4617  frd  5539  xpdifid  6060  funeldmdif  7862  ressuppssdif  7972  oaf1o  8356  findcard2d  8911  cantnflem1  9377  cantnflem2  9378  fin23lem26  10012  isf34lem4  10064  isfin7-2  10083  axdc3lem4  10140  axdc4lem  10142  ttukeylem7  10202  pwfseqlem1  10345  pwfseqlem3  10347  hashf1lem1  14096  hashf1lem1OLD  14097  seqcoll  14106  seqcoll2  14107  rlimcld2  15215  sumrblem  15351  fsumcvg  15352  fsumss  15365  incexclem  15476  prodrblem  15567  fprodcvg  15568  fprodss  15586  fprodn0f  15629  ruclem12  15878  sqrt2irr0  15888  coprmproddvdslem  16295  nnoddn2prmb  16442  prmreclem5  16549  ramub1lem1  16655  mreexd  17268  frgpnabllem1  19389  gsumzaddlem  19437  gsum2d  19488  gsumxp2  19496  dmdprdsplitlem  19555  pgpfac1lem2  19593  pgpfac1lem3  19595  irredrmul  19864  lsppratlem3  20326  lbsextlem4  20338  psgnodpmr  20707  frlmsslsp  20913  regsep2  22435  1stckgen  22613  regr1lem  22798  opnsubg  23167  zcld  23882  recld2  23883  bcthlem4  24396  iundisj  24617  iblss2  24875  itgeqa  24883  limcnlp  24947  dvloglem  25708  dvlog2lem  25712  2irrexpq  25790  logbgcd1irr  25849  ressatans  25989  regamcl  26115  facgam  26120  wilthlem2  26123  2lgslem2  26448  tgelrnln  26895  incistruhgr  27352  upgrres1  27583  usgr2pthlem  28032  iundisjf  30829  iundisjfi  31019  cycpmfv3  31284  cyc3conja  31326  submateqlem1  31659  submateqlem2  31660  elzrhunit  31829  qqhval2  31832  esumrnmpt2  31936  inelpisys  32022  plymulx  32427  ttrcltr  33702  noetasuplem4  33866  noetainflem4  33870  onint1  34565  lindsadd  35697  lindsenlbs  35699  poimirlem23  35727  poimirlem30  35734  dvasin  35788  areacirclem4  35795  pridlc3  36158  relogbzexpd  39910  dvrelog2b  40002  dvrelogpow2b  40004  aks4d1p1p4  40007  aks4d1p6  40017  nelsubginvcld  40146  nelsubgcld  40147  rtprmirr  40268  prjspersym  40367  prjspreln0  40369  prjspvs  40370  prjspnvs  40380  rmspecsqrtnq  40644  rmspecnonsq  40645  pr2eldif1  41050  pr2eldif2  41051  disjf1o  42618  difmap  42636  difmapsn  42641  supminfxr2  42899  icoiccdif  42952  iccdificc  42967  climrec  43034  limciccioolb  43052  limcrecl  43060  sumnnodd  43061  lptioo2  43062  lptioo1  43063  limcicciooub  43068  lptre2pt  43071  reclimc  43084  cnrefiisplem  43260  icccncfext  43318  fperdvper  43350  dvnmul  43374  itgcoscmulx  43400  itgsincmulx  43405  stoweidlem34  43465  stoweidlem39  43470  stoweidlem57  43488  wallispi  43501  stirlinglem8  43512  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem38  43576  fourierdlem40  43578  fourierdlem42  43580  fourierdlem46  43583  fourierdlem53  43590  fourierdlem56  43593  fourierdlem58  43595  fourierdlem62  43599  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  elaa2  43665  etransc  43714  gsumge0cl  43799  sge0fodjrnlem  43844  iundjiun  43888  meadjiunlem  43893  meaiininclem  43914  caragendifcl  43942  caratheodorylem1  43954  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem4  44026  hspdifhsp  44044  hspmbllem2  44055  preimagelt  44126  preimalegt  44127  sqrtnegnre  44687  requad01  44961  dig1  45842