MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifd Structured version   Visualization version   GIF version

Theorem eldifd 3926
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3925. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
eldifd.1 (𝜑𝐴𝐵)
eldifd.2 (𝜑 → ¬ 𝐴𝐶)
Assertion
Ref Expression
eldifd (𝜑𝐴 ∈ (𝐵𝐶))

Proof of Theorem eldifd
StepHypRef Expression
1 eldifd.1 . 2 (𝜑𝐴𝐵)
2 eldifd.2 . 2 (𝜑 → ¬ 𝐴𝐶)
3 eldif 3925 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
41, 2, 3sylanbrc 584 1 (𝜑𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  cdif 3912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918
This theorem is referenced by:  rexdifi  4110  eqoreldif  4650  frd  5597  xpdifid  6125  funeldmdif  7985  ressuppssdif  8121  oaf1o  8515  findcard2d  9117  cantnflem1  9632  cantnflem2  9633  ttrcltr  9659  fin23lem26  10268  isf34lem4  10320  isfin7-2  10339  axdc3lem4  10396  axdc4lem  10398  ttukeylem7  10458  pwfseqlem1  10601  pwfseqlem3  10603  hashf1lem1  14360  hashf1lem1OLD  14361  seqcoll  14370  seqcoll2  14371  rlimcld2  15467  sumrblem  15603  fsumcvg  15604  fsumss  15617  incexclem  15728  prodrblem  15819  fprodcvg  15820  fprodss  15838  fprodn0f  15881  ruclem12  16130  sqrt2irr0  16140  coprmproddvdslem  16545  nnoddn2prmb  16692  prmreclem5  16799  ramub1lem1  16905  mreexd  17529  frgpnabllem1  19658  gsumzaddlem  19705  gsum2d  19756  gsumxp2  19764  dmdprdsplitlem  19823  pgpfac1lem2  19861  pgpfac1lem3  19863  irredrmul  20145  lsppratlem3  20626  lbsextlem4  20638  psgnodpmr  21010  frlmsslsp  21218  regsep2  22743  1stckgen  22921  regr1lem  23106  opnsubg  23475  zcld  24192  recld2  24193  bcthlem4  24707  iundisj  24928  iblss2  25186  itgeqa  25194  limcnlp  25258  dvloglem  26019  dvlog2lem  26023  2irrexpq  26101  logbgcd1irr  26160  ressatans  26300  regamcl  26426  facgam  26431  wilthlem2  26434  2lgslem2  26759  noetasuplem4  27100  noetainflem4  27104  mulsval  27396  tgelrnln  27614  incistruhgr  28072  upgrres1  28303  usgr2pthlem  28753  iundisjf  31549  iundisjfi  31741  cycpmfv3  32006  cyc3conja  32048  submateqlem1  32428  submateqlem2  32429  elzrhunit  32600  qqhval2  32603  esumrnmpt2  32707  inelpisys  32793  plymulx  33200  onint1  34950  lindsadd  36100  lindsenlbs  36102  poimirlem23  36130  poimirlem30  36137  dvasin  36191  areacirclem4  36198  pridlc3  36561  relogbzexpd  40461  dvrelog2b  40552  dvrelogpow2b  40554  aks4d1p1p4  40557  aks4d1p6  40567  nelsubginvcld  40700  nelsubgcld  40701  rtprmirr  40862  prjspersym  40974  prjspreln0  40976  prjspvs  40977  prjspnvs  40987  rmspecsqrtnq  41258  rmspecnonsq  41259  pr2eldif1  41900  pr2eldif2  41901  disjf1o  43484  difmap  43502  difmapsn  43507  supminfxr2  43778  icoiccdif  43836  iccdificc  43851  climrec  43918  limciccioolb  43936  limcrecl  43944  sumnnodd  43945  lptioo2  43946  lptioo1  43947  limcicciooub  43952  lptre2pt  43955  reclimc  43968  cnrefiisplem  44144  icccncfext  44202  fperdvper  44234  dvnmul  44258  itgcoscmulx  44284  itgsincmulx  44289  stoweidlem34  44349  stoweidlem39  44354  stoweidlem57  44372  wallispi  44385  stirlinglem8  44396  dirkercncflem2  44419  dirkercncflem4  44421  fourierdlem38  44460  fourierdlem40  44462  fourierdlem42  44464  fourierdlem46  44467  fourierdlem53  44474  fourierdlem56  44477  fourierdlem58  44479  fourierdlem62  44483  fourierdlem74  44495  fourierdlem75  44496  fourierdlem76  44497  fourierdlem78  44499  fourierdlem93  44514  fourierdlem103  44524  fourierdlem104  44525  fouriersw  44546  elaa2  44549  etransc  44598  gsumge0cl  44686  sge0fodjrnlem  44731  iundjiun  44775  meadjiunlem  44780  meaiininclem  44801  caragendifcl  44829  caratheodorylem1  44841  hoidmvlelem1  44910  hoidmvlelem2  44911  hoidmvlelem4  44913  hspdifhsp  44931  hspmbllem2  44942  preimagelt  45014  preimalegt  45015  sqrtnegnre  45613  requad01  45887  dig1  46768
  Copyright terms: Public domain W3C validator