Theorem eldifd 4053

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050

This theorem is used by:  rexdifi  4089  eqoreldif  4646  frd  5612  xpdifid  6165  xpdifcnvepel  6166  funeldmdif  8070  ressuppssdif  8216  oaf1o  8585  findcard2d  9196  cantnflem1  9703  cantnflem2  9704  ttrcltr  9730  fin23lem26  10416  isf34lem4  10468  isfin7-2  10487  axdc3lem4  10544  axdc4lem  10546  ttukeylem7  10606  pwfseqlem1  10756  pwfseqlem3  10758  hashf1lem1  14613  seqcoll  14622  seqcoll2  14623  rlimcld2  15760  sumrblem  15892  fsumcvg  15893  fsumss  15906  incexclem  16020  prodrblem  16111  fprodcvg  16112  fprodss  16130  fprodn0f  16173  ruclem12  16424  sqrt2irr0  16434  coprmproddvdslem  16852  nnoddn2prmb  17006  prmreclem5  17113  ramub1lem1  17219  mreexd  17831  chnccats1  18814  chnccat  18815  frgpnabllem1  20102  gsumzaddlem  20150  gsum2d  20201  gsumxp2  20209  dmdprdsplitlem  20268  pgpfac1lem2  20306  pgpfac1lem3  20308  irredrmul  20672  lsppratlem3  21442  lbsextlem4  21454  cmprmidlmcl  21646  prmidlsubm  21658  psgnodpmr  21911  frlmsslsp  22117  lindsenlbs  22172  regsep2  23709  1stckgen  23888  regr1lem  24073  opnsubg  24442  zcld  25148  recld2  25149  bcthlem4  25663  iundisj  25884  iblss2  26141  itgeqa  26149  limcnlp  26213  plymulidp  26618  dvloglem  26991  dvlog2lem  26995  2irrexpq  27074  rtprmirr  27103  logbgcd1irr  27137  ressatans  27277  regamcl  27403  facgam  27408  wilthlem2  27411  2lgslem2  27737  noetasuplem4  28108  noetainflem4  28112  mulsval  28510  tgelrnln  29113  tglnpt4  29138  tgelrnpln  29269  lnincplng  29277  plngcplem  29278  plngrotlem1  29280  plngrotlem2  29281  lnssplnglem  29284  lnssplng  29285  nhpmirhp  29291  perpeq  29363  tgaaddcpbllem1  29364  tgaaddcpbl  29367  tgaaddcpbl2  29368  prlnghpg  29439  dfprlng2  29440  prlngpln3  29442  prlngex  29444  prlngmolem2  29446  prlngmo2  29449  prlngpln4  29451  symquadprlng  29455  prlngsymquadlem  29456  quadcgrprlng  29459  incistruhgr  29672  upgrres1  29909  dfpth2  30329  usgr2pthlem  30364  iundisjf  33240  iundisjfi  33444  gsumfs2d  33678  cycpmfv3  33732  cyc3conja  33774  elrgspnlem4  33862  elrgspnsubrunlem2  33865  mxidlirredi  34052  qsdrngilem  34074  dflringlem2  34083  dflring3  34085  rsprprmprmidlb  34111  rprmirred  34119  rprmirredb  34120  1arithufdlem3  34134  dfufd2  34138  ply1dg3rt0irred  34172  ig1pmindeg  34190  selvascl  34205  esplyfv  34258  esplyfval3  34260  esplyfvn  34265  fldextrspunlsplem  34361  fldextrspunlsp  34362  submateqlem1  34495  submateqlem2  34496  elzrhunit  34665  qqhval2  34670  esumrnmpt2  34756  inelpisys  34843  nmulprop  37069  onint1  37367  mh-inf3sn  37460  lindsadd  38679  poimirlem23  38704  poimirlem30  38711  dvasin  38765  areacirclem4  38772  pridlc3  39150  relogbzexpd  43169  dvrelog2b  43259  dvrelogpow2b  43261  aks4d1p1p4  43264  aks4d1p6  43274  aks6d1c7lem1  43373  nelsubginvcld  43703  nelsubgcld  43704  prjspersym  43778  prjspreln0  43780  prjspnvs  43791  rmspecsqrtnq  44056  rmspecnonsq  44057  pr2eldif1  44698  pr2eldif2  44699  disjf1o  46348  difmap  46362  difmapsn  46367  supminfxr2  46621  icoiccdif  46678  iccdificc  46693  climrec  46757  limciccioolb  46775  limcrecl  46783  sumnnodd  46784  lptioo2  46785  lptioo1  46786  limcicciooub  46789  lptre2pt  46792  reclimc  46805  cnrefiisplem  46981  icccncfext  47039  fperdvper  47071  dvnmul  47095  itgcoscmulx  47121  itgsincmulx  47126  stoweidlem34  47186  stoweidlem39  47191  stoweidlem57  47209  wallispi  47222  stirlinglem8  47233  dirkercncflem2  47256  dirkercncflem4  47258  fourierdlem38  47297  fourierdlem40  47299  fourierdlem42  47301  fourierdlem46  47304  fourierdlem53  47311  fourierdlem56  47314  fourierdlem58  47316  fourierdlem62  47320  fourierdlem74  47332  fourierdlem75  47333  fourierdlem76  47334  fourierdlem78  47336  fourierdlem93  47351  fourierdlem103  47361  fourierdlem104  47362  fouriersw  47383  elaa2  47386  etransc  47435  gsumge0cl  47523  sge0fodjrnlem  47568  iundjiun  47612  meadjiunlem  47617  meaiininclem  47638  caragendifcl  47666  caratheodorylem1  47678  hoidmvlelem1  47747  hoidmvlelem2  47748  hoidmvlelem4  47750  hspdifhsp  47768  hspmbllem2  47779  preimagelt  47851  preimalegt  47852  sqrtnegnre  48519  requad01  48861  dig1  49862