Theorem eldifd 3894

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886

This theorem is referenced by:  rexdifi  4081  eqoreldif  4618  frd  5576  xpdifid  6120  funeldmdif  7991  ressuppssdif  8126  oaf1o  8489  findcard2d  9092  cantnflem1  9602  cantnflem2  9603  ttrcltr  9629  fin23lem26  10239  isf34lem4  10291  isfin7-2  10310  axdc3lem4  10367  axdc4lem  10369  ttukeylem7  10429  pwfseqlem1  10573  pwfseqlem3  10575  hashf1lem1  14409  seqcoll  14418  seqcoll2  14419  rlimcld2  15532  sumrblem  15665  fsumcvg  15666  fsumss  15679  incexclem  15793  prodrblem  15886  fprodcvg  15887  fprodss  15905  fprodn0f  15948  ruclem12  16200  sqrt2irr0  16210  coprmproddvdslem  16623  nnoddn2prmb  16776  prmreclem5  16883  ramub1lem1  16989  mreexd  17600  chnccats1  18583  chnccat  18584  frgpnabllem1  19840  gsumzaddlem  19888  gsum2d  19939  gsumxp2  19947  dmdprdsplitlem  20006  pgpfac1lem2  20044  pgpfac1lem3  20046  irredrmul  20399  lsppratlem3  21143  lbsextlem4  21155  psgnodpmr  21566  frlmsslsp  21772  regsep2  23360  1stckgen  23538  regr1lem  23723  opnsubg  24092  zcld  24798  recld2  24799  bcthlem4  25313  iundisj  25534  iblss2  25792  itgeqa  25800  limcnlp  25864  dvloglem  26631  dvlog2lem  26635  2irrexpq  26714  rtprmirr  26743  logbgcd1irr  26777  ressatans  26917  regamcl  27043  facgam  27048  wilthlem2  27051  2lgslem2  27377  noetasuplem4  27719  noetainflem4  27723  mulsval  28120  tgelrnln  28717  incistruhgr  29167  upgrres1  29401  dfpth2  29816  usgr2pthlem  29850  iundisjf  32679  iundisjfi  32889  gsumfs2d  33143  cycpmfv3  33197  cyc3conja  33239  elrgspnlem4  33327  elrgspnsubrunlem2  33330  mxidlirredi  33555  qsdrngilem  33578  dflringlem2  33587  dflring3  33589  rsprprmprmidlb  33615  rprmirred  33623  rprmirredb  33624  1arithufdlem3  33638  dfufd2  33642  ply1dg3rt0irred  33676  ig1pmindeg  33694  selvascl  33710  esplyfv  33763  esplyfval3  33765  esplyfvn  33770  fldextrspunlsplem  33866  fldextrspunlsp  33867  submateqlem1  34000  submateqlem2  34001  elzrhunit  34170  qqhval2  34175  esumrnmpt2  34261  inelpisys  34347  plymulx  34741  onint1  36686  mh-inf3sn  36779  lindsadd  37989  lindsenlbs  37991  poimirlem23  38019  poimirlem30  38026  dvasin  38080  areacirclem4  38087  pridlc3  38449  relogbzexpd  42470  dvrelog2b  42560  dvrelogpow2b  42562  aks4d1p1p4  42565  aks4d1p6  42575  aks6d1c7lem1  42674  nelsubginvcld  42995  nelsubgcld  42996  prjspersym  43066  prjspreln0  43068  prjspnvs  43079  rmspecsqrtnq  43360  rmspecnonsq  43361  pr2eldif1  44007  pr2eldif2  44008  disjf1o  45646  difmap  45660  difmapsn  45665  supminfxr2  45920  icoiccdif  45977  iccdificc  45992  climrec  46056  limciccioolb  46074  limcrecl  46082  sumnnodd  46083  lptioo2  46084  lptioo1  46085  limcicciooub  46088  lptre2pt  46091  reclimc  46104  cnrefiisplem  46280  icccncfext  46338  fperdvper  46370  dvnmul  46394  itgcoscmulx  46420  itgsincmulx  46425  stoweidlem34  46485  stoweidlem39  46490  stoweidlem57  46508  wallispi  46521  stirlinglem8  46532  dirkercncflem2  46555  dirkercncflem4  46557  fourierdlem38  46596  fourierdlem40  46598  fourierdlem42  46600  fourierdlem46  46603  fourierdlem53  46610  fourierdlem56  46613  fourierdlem58  46615  fourierdlem62  46619  fourierdlem74  46631  fourierdlem75  46632  fourierdlem76  46633  fourierdlem78  46635  fourierdlem93  46650  fourierdlem103  46660  fourierdlem104  46661  fouriersw  46682  elaa2  46685  etransc  46734  gsumge0cl  46822  sge0fodjrnlem  46867  iundjiun  46911  meadjiunlem  46916  meaiininclem  46937  caragendifcl  46965  caratheodorylem1  46977  hoidmvlelem1  47046  hoidmvlelem2  47047  hoidmvlelem4  47049  hspdifhsp  47067  hspmbllem2  47078  preimagelt  47150  preimalegt  47151  sqrtnegnre  47778  requad01  48120  dig1  49107