Theorem eldifd 3803

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-dif 3795

This theorem is referenced by:  eqoreldif  4453  xpdifid  5816  ressuppssdif  7597  oaf1o  7927  findcard2d  8490  cantnflem1  8883  cantnflem2  8884  fin23lem26  9482  isf34lem4  9534  isfin7-2  9553  axdc3lem4  9610  axdc4lem  9612  ttukeylem7  9672  pwfseqlem1  9815  pwfseqlem3  9817  hashf1lem1  13553  seqcoll  13562  seqcoll2  13563  rlimcld2  14717  sumrblem  14849  fsumcvg  14850  fsumss  14863  incexclem  14972  prodrblem  15062  fprodcvg  15063  fprodss  15081  fprodn0f  15124  ruclem12  15374  sqrt2irr0  15384  coprmproddvdslem  15781  nnoddn2prmb  15922  prmreclem5  16028  ramub1lem1  16134  mreexd  16688  frgpnabllem1  18662  gsumzaddlem  18707  gsum2d  18757  dmdprdsplitlem  18823  pgpfac1lem2  18861  pgpfac1lem3  18863  irredrmul  19094  lsppratlem3  19546  lbsextlem4  19558  psgnodpmr  20331  frlmsslsp  20539  regsep2  21588  1stckgen  21766  regr1lem  21951  opnsubg  22319  zcld  23024  recld2  23025  bcthlem4  23533  iundisj  23752  iblss2  24009  itgeqa  24017  limcnlp  24079  dvloglem  24831  dvlog2lem  24835  2irrexpq  24913  logbgcd1irr  24972  ressatans  25112  regamcl  25239  facgam  25244  wilthlem2  25247  2lgslem2  25572  tgelrnln  25981  incistruhgr  26427  upgrres1  26660  usgr2pthlem  27115  iundisjf  29965  iundisjfi  30119  submateqlem1  30471  submateqlem2  30472  elzrhunit  30621  qqhval2  30624  esumrnmpt2  30728  inelpisys  30815  plymulx  31225  signstfvneq0  31250  noetalem3  32454  onint1  33031  lindsadd  34028  lindsenlbs  34030  poimirlem23  34058  poimirlem30  34065  dvasin  34121  areacirclem4  34128  pridlc3  34496  nelsubginvcld  38131  nelsubgcld  38132  rtprmirr  38172  prjspersym  38208  rmspecsqrtnq  38430  rmspecnonsq  38431  disjf1o  40301  difmap  40320  difmapsn  40325  supminfxr2  40604  icoiccdif  40659  iccdificc  40674  climrec  40743  limciccioolb  40761  limcrecl  40769  sumnnodd  40770  lptioo2  40771  lptioo1  40772  limcicciooub  40777  lptre2pt  40780  reclimc  40793  cnrefiisplem  40969  icccncfext  41028  fperdvper  41061  dvnmul  41086  itgcoscmulx  41112  itgsincmulx  41117  stoweidlem34  41178  stoweidlem39  41183  stoweidlem57  41201  wallispi  41214  stirlinglem8  41225  dirkercncflem2  41248  dirkercncflem4  41250  fourierdlem38  41289  fourierdlem40  41291  fourierdlem42  41293  fourierdlem46  41296  fourierdlem53  41303  fourierdlem56  41306  fourierdlem58  41308  fourierdlem62  41312  fourierdlem74  41324  fourierdlem75  41325  fourierdlem76  41326  fourierdlem78  41328  fourierdlem93  41343  fourierdlem103  41353  fourierdlem104  41354  fouriersw  41375  elaa2  41378  etransc  41427  gsumge0cl  41512  sge0fodjrnlem  41557  iundjiun  41601  meadjiunlem  41606  meaiininclem  41627  caragendifcl  41655  caratheodorylem1  41667  hoidmvlelem1  41736  hoidmvlelem2  41737  hoidmvlelem4  41739  hspdifhsp  41757  hspmbllem2  41768  preimagelt  41839  preimalegt  41840  sqrtnegnre  42349  requad01  42559  dig1  43417