Theorem eldifd 3900

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ∖ cdif 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892

This theorem is referenced by:  rexdifi  4090  eqoreldif  4629  frd  5588  xpdifid  6132  funeldmdif  8001  ressuppssdif  8135  oaf1o  8498  findcard2d  9101  cantnflem1  9610  cantnflem2  9611  ttrcltr  9637  fin23lem26  10247  isf34lem4  10299  isfin7-2  10318  axdc3lem4  10375  axdc4lem  10377  ttukeylem7  10437  pwfseqlem1  10581  pwfseqlem3  10583  hashf1lem1  14417  seqcoll  14426  seqcoll2  14427  rlimcld2  15540  sumrblem  15673  fsumcvg  15674  fsumss  15687  incexclem  15801  prodrblem  15894  fprodcvg  15895  fprodss  15913  fprodn0f  15956  ruclem12  16208  sqrt2irr0  16218  coprmproddvdslem  16631  nnoddn2prmb  16784  prmreclem5  16891  ramub1lem1  16997  mreexd  17608  chnccats1  18591  chnccat  18592  frgpnabllem1  19848  gsumzaddlem  19896  gsum2d  19947  gsumxp2  19955  dmdprdsplitlem  20014  pgpfac1lem2  20052  pgpfac1lem3  20054  irredrmul  20407  lsppratlem3  21147  lbsextlem4  21159  psgnodpmr  21570  frlmsslsp  21776  regsep2  23341  1stckgen  23519  regr1lem  23704  opnsubg  24073  zcld  24779  recld2  24780  bcthlem4  25294  iundisj  25515  iblss2  25773  itgeqa  25781  limcnlp  25845  dvloglem  26612  dvlog2lem  26616  2irrexpq  26695  rtprmirr  26724  logbgcd1irr  26758  ressatans  26898  regamcl  27024  facgam  27029  wilthlem2  27032  2lgslem2  27358  noetasuplem4  27700  noetainflem4  27704  mulsval  28101  tgelrnln  28698  incistruhgr  29148  upgrres1  29382  dfpth2  29797  usgr2pthlem  29831  iundisjf  32659  iundisjfi  32869  gsumfs2d  33122  cycpmfv3  33176  cyc3conja  33218  elrgspnlem4  33306  elrgspnsubrunlem2  33309  mxidlirredi  33531  qsdrngilem  33554  rsprprmprmidlb  33583  rprmirred  33591  rprmirredb  33592  1arithufdlem3  33606  dfufd2  33610  ply1dg3rt0irred  33644  ig1pmindeg  33662  esplyfv  33714  esplyfval3  33716  esplyfvn  33721  fldextrspunlsplem  33817  fldextrspunlsp  33818  submateqlem1  33951  submateqlem2  33952  elzrhunit  34121  qqhval2  34126  esumrnmpt2  34212  inelpisys  34298  plymulx  34692  onint1  36631  mh-inf3sn  36724  lindsadd  37934  lindsenlbs  37936  poimirlem23  37964  poimirlem30  37971  dvasin  38025  areacirclem4  38032  pridlc3  38394  relogbzexpd  42415  dvrelog2b  42505  dvrelogpow2b  42507  aks4d1p1p4  42510  aks4d1p6  42520  aks6d1c7lem1  42619  nelsubginvcld  42941  nelsubgcld  42942  prjspersym  43040  prjspreln0  43042  prjspnvs  43053  rmspecsqrtnq  43334  rmspecnonsq  43335  pr2eldif1  43981  pr2eldif2  43982  disjf1o  45621  difmap  45636  difmapsn  45641  supminfxr2  45897  icoiccdif  45954  iccdificc  45969  climrec  46033  limciccioolb  46051  limcrecl  46059  sumnnodd  46060  lptioo2  46061  lptioo1  46062  limcicciooub  46065  lptre2pt  46068  reclimc  46081  cnrefiisplem  46257  icccncfext  46315  fperdvper  46347  dvnmul  46371  itgcoscmulx  46397  itgsincmulx  46402  stoweidlem34  46462  stoweidlem39  46467  stoweidlem57  46485  wallispi  46498  stirlinglem8  46509  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem38  46573  fourierdlem40  46575  fourierdlem42  46577  fourierdlem46  46580  fourierdlem53  46587  fourierdlem56  46590  fourierdlem58  46592  fourierdlem62  46596  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  elaa2  46662  etransc  46711  gsumge0cl  46799  sge0fodjrnlem  46844  iundjiun  46888  meadjiunlem  46893  meaiininclem  46914  caragendifcl  46942  caratheodorylem1  46954  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem4  47026  hspdifhsp  47044  hspmbllem2  47055  preimagelt  47127  preimalegt  47128  sqrtnegnre  47755  requad01  48097  dig1  49084