Theorem eldifd 3956

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2099   ∖ cdif 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-dif 3948

This theorem is referenced by:  rexdifi  4141  eqoreldif  4684  frd  5631  xpdifid  6166  funeldmdif  8046  ressuppssdif  8183  oaf1o  8577  findcard2d  9184  cantnflem1  9706  cantnflem2  9707  ttrcltr  9733  fin23lem26  10342  isf34lem4  10394  isfin7-2  10413  axdc3lem4  10470  axdc4lem  10472  ttukeylem7  10532  pwfseqlem1  10675  pwfseqlem3  10677  hashf1lem1  14441  hashf1lem1OLD  14442  seqcoll  14451  seqcoll2  14452  rlimcld2  15548  sumrblem  15683  fsumcvg  15684  fsumss  15697  incexclem  15808  prodrblem  15899  fprodcvg  15900  fprodss  15918  fprodn0f  15961  ruclem12  16211  sqrt2irr0  16221  coprmproddvdslem  16626  nnoddn2prmb  16775  prmreclem5  16882  ramub1lem1  16988  mreexd  17615  frgpnabllem1  19821  gsumzaddlem  19869  gsum2d  19920  gsumxp2  19928  dmdprdsplitlem  19987  pgpfac1lem2  20025  pgpfac1lem3  20027  irredrmul  20359  lsppratlem3  21030  lbsextlem4  21042  psgnodpmr  21515  frlmsslsp  21723  regsep2  23273  1stckgen  23451  regr1lem  23636  opnsubg  24005  zcld  24722  recld2  24723  bcthlem4  25248  iundisj  25470  iblss2  25728  itgeqa  25736  limcnlp  25800  dvloglem  26575  dvlog2lem  26579  2irrexpq  26658  logbgcd1irr  26719  ressatans  26859  regamcl  26986  facgam  26991  wilthlem2  26994  2lgslem2  27321  noetasuplem4  27662  noetainflem4  27666  mulsval  28002  tgelrnln  28427  incistruhgr  28885  upgrres1  29119  usgr2pthlem  29570  iundisjf  32372  iundisjfi  32558  cycpmfv3  32830  cyc3conja  32872  mxidlirredi  33178  qsdrngilem  33199  ig1pmindeg  33262  submateqlem1  33402  submateqlem2  33403  elzrhunit  33574  qqhval2  33577  esumrnmpt2  33681  inelpisys  33767  plymulx  34174  onint1  35927  lindsadd  37080  lindsenlbs  37082  poimirlem23  37110  poimirlem30  37117  dvasin  37171  areacirclem4  37178  pridlc3  37540  relogbzexpd  41439  dvrelog2b  41531  dvrelogpow2b  41533  aks4d1p1p4  41536  aks4d1p6  41546  aks6d1c7lem1  41646  nelsubginvcld  41730  nelsubgcld  41731  rtprmirr  41900  prjspersym  42025  prjspreln0  42027  prjspvs  42028  prjspnvs  42038  rmspecsqrtnq  42320  rmspecnonsq  42321  pr2eldif1  42978  pr2eldif2  42979  disjf1o  44558  difmap  44574  difmapsn  44579  supminfxr2  44845  icoiccdif  44903  iccdificc  44918  climrec  44985  limciccioolb  45003  limcrecl  45011  sumnnodd  45012  lptioo2  45013  lptioo1  45014  limcicciooub  45019  lptre2pt  45022  reclimc  45035  cnrefiisplem  45211  icccncfext  45269  fperdvper  45301  dvnmul  45325  itgcoscmulx  45351  itgsincmulx  45356  stoweidlem34  45416  stoweidlem39  45421  stoweidlem57  45439  wallispi  45452  stirlinglem8  45463  dirkercncflem2  45486  dirkercncflem4  45488  fourierdlem38  45527  fourierdlem40  45529  fourierdlem42  45531  fourierdlem46  45534  fourierdlem53  45541  fourierdlem56  45544  fourierdlem58  45546  fourierdlem62  45550  fourierdlem74  45562  fourierdlem75  45563  fourierdlem76  45564  fourierdlem78  45566  fourierdlem93  45581  fourierdlem103  45591  fourierdlem104  45592  fouriersw  45613  elaa2  45616  etransc  45665  gsumge0cl  45753  sge0fodjrnlem  45798  iundjiun  45842  meadjiunlem  45847  meaiininclem  45868  caragendifcl  45896  caratheodorylem1  45908  hoidmvlelem1  45977  hoidmvlelem2  45978  hoidmvlelem4  45980  hspdifhsp  45998  hspmbllem2  46009  preimagelt  46081  preimalegt  46082  sqrtnegnre  46681  requad01  46955  dig1  47675

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »