Theorem eldifd 3745

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2155   ∖ cdif 3731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3737

This theorem is referenced by:  eqoreldif  4384  xpdifid  5747  ressuppssdif  7520  oaf1o  7850  findcard2d  8411  cantnflem1  8803  cantnflem2  8804  fin23lem26  9402  isf34lem4  9454  isfin7-2  9473  axdc3lem4  9530  axdc4lem  9532  ttukeylem7  9592  pwfseqlem1  9735  pwfseqlem3  9737  hashf1lem1  13443  seqcoll  13452  seqcoll2  13453  rlimcld2  14597  sumrblem  14730  fsumcvg  14731  fsumss  14744  incexclem  14855  prodrblem  14945  fprodcvg  14946  fprodss  14964  fprodn0f  15007  ruclem12  15255  coprmproddvdslem  15659  nnoddn2prmb  15800  prmreclem5  15906  ramub1lem1  16012  mreexd  16571  frgpnabllem1  18545  gsumzaddlem  18590  gsum2d  18640  dmdprdsplitlem  18706  pgpfac1lem2  18744  pgpfac1lem3  18746  irredrmul  18977  lsppratlem3  19426  lbsextlem4  19438  psgnodpmr  20211  frlmsslsp  20414  regsep2  21463  1stckgen  21640  regr1lem  21825  opnsubg  22193  zcld  22898  recld2  22899  bcthlem4  23407  iundisj  23609  iblss2  23866  itgeqa  23874  limcnlp  23936  dvloglem  24688  dvlog2lem  24692  ressatans  24955  regamcl  25081  facgam  25086  wilthlem2  25089  2lgslem2  25414  tgelrnln  25819  incistruhgr  26254  upgrres1  26487  usgr2pthlem  26954  iundisjf  29853  iundisjfi  30007  submateqlem1  30323  submateqlem2  30324  elzrhunit  30473  qqhval2  30476  esumrnmpt2  30580  inelpisys  30667  plymulx  31077  signstfvneq0  31102  noetalem3  32312  onint1  32890  lindsenlbs  33831  poimirlem23  33859  poimirlem30  33866  dvasin  33922  areacirclem4  33929  pridlc3  34297  rmspecsqrtnq  38151  rmspecnonsq  38152  disjf1o  40028  difmap  40047  difmapsn  40052  supminfxr2  40339  icoiccdif  40392  iccdificc  40407  climrec  40476  limciccioolb  40494  limcrecl  40502  sumnnodd  40503  lptioo2  40504  lptioo1  40505  limcicciooub  40510  lptre2pt  40513  reclimc  40526  cnrefiisplem  40696  icccncfext  40741  fperdvper  40774  dvnmul  40799  itgcoscmulx  40825  itgsincmulx  40830  stoweidlem34  40891  stoweidlem39  40896  stoweidlem57  40914  wallispi  40927  stirlinglem8  40938  dirkercncflem2  40961  dirkercncflem4  40963  fourierdlem38  41002  fourierdlem40  41004  fourierdlem42  41006  fourierdlem46  41009  fourierdlem53  41016  fourierdlem56  41019  fourierdlem58  41021  fourierdlem62  41025  fourierdlem74  41037  fourierdlem75  41038  fourierdlem76  41039  fourierdlem78  41041  fourierdlem93  41056  fourierdlem103  41066  fourierdlem104  41067  fouriersw  41088  elaa2  41091  etransc  41140  gsumge0cl  41228  sge0fodjrnlem  41273  iundjiun  41317  meadjiunlem  41322  meaiininclem  41343  caragendifcl  41371  caratheodorylem1  41383  hoidmvlelem1  41452  hoidmvlelem2  41453  hoidmvlelem4  41455  hspdifhsp  41473  hspmbllem2  41484  preimagelt  41555  preimalegt  41556  dig1  43074