Theorem eldifd 3955

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2098   ∖ cdif 3941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947

This theorem is referenced by:  rexdifi  4142  eqoreldif  4690  frd  5637  xpdifid  6174  funeldmdif  8053  ressuppssdif  8190  oaf1o  8584  findcard2d  9191  cantnflem1  9714  cantnflem2  9715  ttrcltr  9741  fin23lem26  10350  isf34lem4  10402  isfin7-2  10421  axdc3lem4  10478  axdc4lem  10480  ttukeylem7  10540  pwfseqlem1  10683  pwfseqlem3  10685  hashf1lem1  14451  hashf1lem1OLD  14452  seqcoll  14461  seqcoll2  14462  rlimcld2  15558  sumrblem  15693  fsumcvg  15694  fsumss  15707  incexclem  15818  prodrblem  15909  fprodcvg  15910  fprodss  15928  fprodn0f  15971  ruclem12  16221  sqrt2irr0  16231  coprmproddvdslem  16636  nnoddn2prmb  16785  prmreclem5  16892  ramub1lem1  16998  mreexd  17625  frgpnabllem1  19840  gsumzaddlem  19888  gsum2d  19939  gsumxp2  19947  dmdprdsplitlem  20006  pgpfac1lem2  20044  pgpfac1lem3  20046  irredrmul  20378  lsppratlem3  21049  lbsextlem4  21061  psgnodpmr  21539  frlmsslsp  21747  regsep2  23324  1stckgen  23502  regr1lem  23687  opnsubg  24056  zcld  24773  recld2  24774  bcthlem4  25299  iundisj  25521  iblss2  25779  itgeqa  25787  limcnlp  25851  dvloglem  26627  dvlog2lem  26631  2irrexpq  26710  logbgcd1irr  26771  ressatans  26911  regamcl  27038  facgam  27043  wilthlem2  27046  2lgslem2  27373  noetasuplem4  27715  noetainflem4  27719  mulsval  28059  tgelrnln  28506  incistruhgr  28964  upgrres1  29198  usgr2pthlem  29649  iundisjf  32458  iundisjfi  32646  cycpmfv3  32928  cyc3conja  32970  mxidlirredi  33283  qsdrngilem  33306  rsprprmprmidlb  33335  rprmirred  33343  rprmirredb  33344  1arithufdlem3  33358  dfufd2  33362  ply1dg3rt0irred  33388  ig1pmindeg  33400  submateqlem1  33536  submateqlem2  33537  elzrhunit  33708  qqhval2  33711  esumrnmpt2  33815  inelpisys  33901  plymulx  34308  onint1  36061  lindsadd  37214  lindsenlbs  37216  poimirlem23  37244  poimirlem30  37251  dvasin  37305  areacirclem4  37312  pridlc3  37674  relogbzexpd  41574  dvrelog2b  41666  dvrelogpow2b  41668  aks4d1p1p4  41671  aks4d1p6  41681  aks6d1c7lem1  41780  nelsubginvcld  41871  nelsubgcld  41872  rtprmirr  42038  prjspersym  42163  prjspreln0  42165  prjspvs  42166  prjspnvs  42176  rmspecsqrtnq  42465  rmspecnonsq  42466  pr2eldif1  43123  pr2eldif2  43124  disjf1o  44700  difmap  44716  difmapsn  44721  supminfxr2  44986  icoiccdif  45044  iccdificc  45059  climrec  45126  limciccioolb  45144  limcrecl  45152  sumnnodd  45153  lptioo2  45154  lptioo1  45155  limcicciooub  45160  lptre2pt  45163  reclimc  45176  cnrefiisplem  45352  icccncfext  45410  fperdvper  45442  dvnmul  45466  itgcoscmulx  45492  itgsincmulx  45497  stoweidlem34  45557  stoweidlem39  45562  stoweidlem57  45580  wallispi  45593  stirlinglem8  45604  dirkercncflem2  45627  dirkercncflem4  45629  fourierdlem38  45668  fourierdlem40  45670  fourierdlem42  45672  fourierdlem46  45675  fourierdlem53  45682  fourierdlem56  45685  fourierdlem58  45687  fourierdlem62  45691  fourierdlem74  45703  fourierdlem75  45704  fourierdlem76  45705  fourierdlem78  45707  fourierdlem93  45722  fourierdlem103  45732  fourierdlem104  45733  fouriersw  45754  elaa2  45757  etransc  45806  gsumge0cl  45894  sge0fodjrnlem  45939  iundjiun  45983  meadjiunlem  45988  meaiininclem  46009  caragendifcl  46037  caratheodorylem1  46049  hoidmvlelem1  46118  hoidmvlelem2  46119  hoidmvlelem4  46121  hspdifhsp  46139  hspmbllem2  46150  preimagelt  46222  preimalegt  46223  sqrtnegnre  46822  requad01  47095  dig1  47864