Theorem eldifd 3910

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902

This theorem is used by:  rexdifi  4097  eqoreldif  4646  frd  5612  xpdifid  6160  xpdifcnvepel  6161  funeldmdif  8046  ressuppssdif  8184  oaf1o  8553  findcard2d  9164  cantnflem1  9671  cantnflem2  9672  ttrcltr  9698  fin23lem26  10330  isf34lem4  10382  isfin7-2  10401  axdc3lem4  10458  axdc4lem  10460  ttukeylem7  10520  pwfseqlem1  10670  pwfseqlem3  10672  hashf1lem1  14523  seqcoll  14532  seqcoll2  14533  rlimcld2  15668  sumrblem  15800  fsumcvg  15801  fsumss  15814  incexclem  15928  prodrblem  16019  fprodcvg  16020  fprodss  16038  fprodn0f  16081  ruclem12  16332  sqrt2irr0  16342  coprmproddvdslem  16755  nnoddn2prmb  16908  prmreclem5  17015  ramub1lem1  17121  mreexd  17733  chnccats1  18716  chnccat  18717  frgpnabllem1  20003  gsumzaddlem  20051  gsum2d  20102  gsumxp2  20110  dmdprdsplitlem  20169  pgpfac1lem2  20207  pgpfac1lem3  20209  irredrmul  20571  lsppratlem3  21339  lbsextlem4  21351  cmprmidlmcl  21541  prmidlsubm  21553  psgnodpmr  21806  frlmsslsp  22012  lindsenlbs  22067  regsep2  23604  1stckgen  23783  regr1lem  23968  opnsubg  24337  zcld  25043  recld2  25044  bcthlem4  25558  iundisj  25779  iblss2  26036  itgeqa  26044  limcnlp  26108  plymulidp  26515  dvloglem  26888  dvlog2lem  26892  2irrexpq  26971  rtprmirr  27000  logbgcd1irr  27034  ressatans  27174  regamcl  27300  facgam  27305  wilthlem2  27308  2lgslem2  27634  noetasuplem4  27975  noetainflem4  27979  mulsval  28377  tgelrnln  28980  tglnpt4  29005  tgelrnpln  29136  lnincplng  29144  plngcplem  29145  plngrotlem1  29147  plngrotlem2  29148  lnssplnglem  29151  lnssplng  29152  nhpmirhp  29158  perpeq  29230  tgaaddcpbllem1  29231  tgaaddcpbl  29234  tgaaddcpbl2  29235  prlnghpg  29306  dfprlng2  29307  prlngpln3  29309  prlngex  29311  prlngmolem2  29313  prlngmo2  29316  prlngpln4  29318  symquadprlng  29322  prlngsymquadlem  29323  quadcgrprlng  29326  incistruhgr  29539  upgrres1  29776  dfpth2  30196  usgr2pthlem  30231  iundisjf  33065  iundisjfi  33270  gsumfs2d  33504  cycpmfv3  33558  cyc3conja  33600  elrgspnlem4  33688  elrgspnsubrunlem2  33691  mxidlirredi  33877  qsdrngilem  33899  dflringlem2  33908  dflring3  33910  rsprprmprmidlb  33936  rprmirred  33944  rprmirredb  33945  1arithufdlem3  33959  dfufd2  33963  ply1dg3rt0irred  33997  ig1pmindeg  34015  selvascl  34030  esplyfv  34083  esplyfval3  34085  esplyfvn  34090  fldextrspunlsplem  34186  fldextrspunlsp  34187  submateqlem1  34320  submateqlem2  34321  elzrhunit  34490  qqhval2  34495  esumrnmpt2  34581  inelpisys  34668  nmulprop  36773  onint1  37071  mh-inf3sn  37164  lindsadd  38370  poimirlem23  38395  poimirlem30  38402  dvasin  38456  areacirclem4  38463  pridlc3  38826  relogbzexpd  42845  dvrelog2b  42935  dvrelogpow2b  42937  aks4d1p1p4  42940  aks4d1p6  42950  aks6d1c7lem1  43049  nelsubginvcld  43387  nelsubgcld  43388  prjspersym  43456  prjspreln0  43458  prjspnvs  43469  rmspecsqrtnq  43750  rmspecnonsq  43751  pr2eldif1  44397  pr2eldif2  44398  disjf1o  46026  difmap  46040  difmapsn  46045  supminfxr2  46300  icoiccdif  46357  iccdificc  46372  climrec  46436  limciccioolb  46454  limcrecl  46462  sumnnodd  46463  lptioo2  46464  lptioo1  46465  limcicciooub  46468  lptre2pt  46471  reclimc  46484  cnrefiisplem  46660  icccncfext  46718  fperdvper  46750  dvnmul  46774  itgcoscmulx  46800  itgsincmulx  46805  stoweidlem34  46865  stoweidlem39  46870  stoweidlem57  46888  wallispi  46901  stirlinglem8  46912  dirkercncflem2  46935  dirkercncflem4  46937  fourierdlem38  46976  fourierdlem40  46978  fourierdlem42  46980  fourierdlem46  46983  fourierdlem53  46990  fourierdlem56  46993  fourierdlem58  46995  fourierdlem62  46999  fourierdlem74  47011  fourierdlem75  47012  fourierdlem76  47013  fourierdlem78  47015  fourierdlem93  47030  fourierdlem103  47040  fourierdlem104  47041  fouriersw  47062  elaa2  47065  etransc  47114  gsumge0cl  47202  sge0fodjrnlem  47247  iundjiun  47291  meadjiunlem  47296  meaiininclem  47317  caragendifcl  47345  caratheodorylem1  47357  hoidmvlelem1  47426  hoidmvlelem2  47427  hoidmvlelem4  47429  hspdifhsp  47447  hspmbllem2  47458  preimagelt  47530  preimalegt  47531  sqrtnegnre  48198  requad01  48540  dig1  49541