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

Theorem eldifd 3578
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3577. (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 3577 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
41, 2, 3sylanbrc 697 1 (𝜑𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1988  cdif 3564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570
This theorem is referenced by:  eqoreldif  4216  eqoreldifOLD  4217  xpdifid  5550  ressuppssdif  7301  oaf1o  7628  findcard2d  8187  cantnflem1  8571  cantnflem2  8572  fin23lem26  9132  isf34lem4  9184  isfin7-2  9203  axdc3lem4  9260  axdc4lem  9262  ttukeylem7  9322  pwfseqlem1  9465  pwfseqlem3  9467  hashf1lem1  13222  seqcoll  13231  seqcoll2  13232  rlimcld2  14290  sumrblem  14423  fsumcvg  14424  fsumss  14437  incexclem  14549  prodrblem  14640  fprodcvg  14641  fprodss  14659  fprodn0f  14703  ruclem12  14951  coprmproddvdslem  15357  nnoddn2prmb  15499  prmreclem5  15605  ramub1lem1  15711  mreexd  16283  frgpnabllem1  18257  gsumzaddlem  18302  gsum2d  18352  dmdprdsplitlem  18417  pgpfac1lem2  18455  pgpfac1lem3  18457  irredrmul  18688  lsppratlem3  19130  lbsextlem4  19142  psgnodpmr  19917  frlmsslsp  20116  regsep2  21161  1stckgen  21338  regr1lem  21523  opnsubg  21892  zcld  22597  recld2  22598  bcthlem4  23105  iundisj  23297  iblss2  23553  itgeqa  23561  limcnlp  23623  dvloglem  24375  dvlog2lem  24379  ressatans  24642  regamcl  24768  facgam  24773  wilthlem2  24776  2lgslem2  25101  tgelrnln  25506  incistruhgr  25955  upgrres1  26186  usgr2pthlem  26640  iundisjf  29374  iundisjfi  29529  submateqlem1  29847  submateqlem2  29848  elzrhunit  29997  qqhval2  30000  esumrnmpt2  30104  inelpisys  30191  plymulx  30599  signstfvneq0  30623  noetalem3  31839  onint1  32423  lindsenlbs  33375  poimirlem23  33403  poimirlem30  33410  dvasin  33467  areacirclem4  33474  pridlc3  33843  rmspecsqrtnq  37289  rmspecsqrtnqOLD  37290  rmspecnonsq  37291  disjf1o  39194  difmap  39215  difmapsn  39220  supminfxr2  39512  icoiccdif  39553  iccdificc  39569  climrec  39635  limciccioolb  39653  limcrecl  39661  sumnnodd  39662  lptioo2  39663  lptioo1  39664  limcicciooub  39669  lptre2pt  39672  reclimc  39685  icccncfext  39863  fperdvper  39896  dvnmul  39921  itgcoscmulx  39948  itgsincmulx  39953  stoweidlem34  40014  stoweidlem39  40019  stoweidlem57  40037  wallispi  40050  stirlinglem8  40061  dirkercncflem2  40084  dirkercncflem4  40086  fourierdlem38  40125  fourierdlem40  40127  fourierdlem42  40129  fourierdlem46  40132  fourierdlem53  40139  fourierdlem56  40142  fourierdlem58  40144  fourierdlem62  40148  fourierdlem74  40160  fourierdlem75  40161  fourierdlem76  40162  fourierdlem78  40164  fourierdlem93  40179  fourierdlem103  40189  fourierdlem104  40190  fouriersw  40211  elaa2  40214  etransc  40263  gsumge0cl  40351  sge0fodjrnlem  40396  iundjiun  40440  meadjiunlem  40445  meaiininclem  40463  caragendifcl  40491  caratheodorylem1  40503  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem4  40575  hspdifhsp  40593  hspmbllem2  40604  preimagelt  40675  preimalegt  40676  dig1  42167
  Copyright terms: Public domain W3C validator