Theorem eldifd 3892

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ∖ cdif 3878

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884

This theorem is referenced by:  rexdifi  4073  eqoreldif  4582  xpdifid  5992  funeldmdif  7729  ressuppssdif  7834  oaf1o  8172  findcard2d  8744  cantnflem1  9136  cantnflem2  9137  fin23lem26  9736  isf34lem4  9788  isfin7-2  9807  axdc3lem4  9864  axdc4lem  9866  ttukeylem7  9926  pwfseqlem1  10069  pwfseqlem3  10071  hashf1lem1  13809  seqcoll  13818  seqcoll2  13819  rlimcld2  14927  sumrblem  15060  fsumcvg  15061  fsumss  15074  incexclem  15183  prodrblem  15275  fprodcvg  15276  fprodss  15294  fprodn0f  15337  ruclem12  15586  sqrt2irr0  15596  coprmproddvdslem  15996  nnoddn2prmb  16140  prmreclem5  16246  ramub1lem1  16352  mreexd  16905  frgpnabllem1  18986  gsumzaddlem  19034  gsum2d  19085  gsumxp2  19093  dmdprdsplitlem  19152  pgpfac1lem2  19190  pgpfac1lem3  19192  irredrmul  19453  lsppratlem3  19914  lbsextlem4  19926  psgnodpmr  20279  frlmsslsp  20485  regsep2  21981  1stckgen  22159  regr1lem  22344  opnsubg  22713  zcld  23418  recld2  23419  bcthlem4  23931  iundisj  24152  iblss2  24409  itgeqa  24417  limcnlp  24481  dvloglem  25239  dvlog2lem  25243  2irrexpq  25321  logbgcd1irr  25380  ressatans  25520  regamcl  25646  facgam  25651  wilthlem2  25654  2lgslem2  25979  tgelrnln  26424  incistruhgr  26872  upgrres1  27103  usgr2pthlem  27552  iundisjf  30352  iundisjfi  30545  cycpmfv3  30807  cyc3conja  30849  submateqlem1  31160  submateqlem2  31161  elzrhunit  31330  qqhval2  31333  esumrnmpt2  31437  inelpisys  31523  plymulx  31928  noetalem3  33332  onint1  33910  lindsadd  35050  lindsenlbs  35052  poimirlem23  35080  poimirlem30  35087  dvasin  35141  areacirclem4  35148  pridlc3  35511  relogbzexpd  39261  nelsubginvcld  39423  nelsubgcld  39424  rtprmirr  39502  prjspersym  39601  prjspreln0  39603  prjspvs  39604  rmspecsqrtnq  39847  rmspecnonsq  39848  pr2eldif1  40253  pr2eldif2  40254  disjf1o  41818  difmap  41836  difmapsn  41841  supminfxr2  42108  icoiccdif  42161  iccdificc  42176  climrec  42245  limciccioolb  42263  limcrecl  42271  sumnnodd  42272  lptioo2  42273  lptioo1  42274  limcicciooub  42279  lptre2pt  42282  reclimc  42295  cnrefiisplem  42471  icccncfext  42529  fperdvper  42561  dvnmul  42585  itgcoscmulx  42611  itgsincmulx  42616  stoweidlem34  42676  stoweidlem39  42681  stoweidlem57  42699  wallispi  42712  stirlinglem8  42723  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem38  42787  fourierdlem40  42789  fourierdlem42  42791  fourierdlem46  42794  fourierdlem53  42801  fourierdlem56  42804  fourierdlem58  42806  fourierdlem62  42810  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem93  42841  fourierdlem103  42851  fourierdlem104  42852  fouriersw  42873  elaa2  42876  etransc  42925  gsumge0cl  43010  sge0fodjrnlem  43055  iundjiun  43099  meadjiunlem  43104  meaiininclem  43125  caragendifcl  43153  caratheodorylem1  43165  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem4  43237  hspdifhsp  43255  hspmbllem2  43266  preimagelt  43337  preimalegt  43338  sqrtnegnre  43864  requad01  44139  dig1  45022