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

Theorem eldifd 3618
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3617. (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 3617 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
41, 2, 3sylanbrc 699 1 (𝜑𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2030  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610
This theorem is referenced by:  eqoreldif  4257  eqoreldifOLD  4258  xpdifid  5597  ressuppssdif  7361  oaf1o  7688  findcard2d  8243  cantnflem1  8624  cantnflem2  8625  fin23lem26  9185  isf34lem4  9237  isfin7-2  9256  axdc3lem4  9313  axdc4lem  9315  ttukeylem7  9375  pwfseqlem1  9518  pwfseqlem3  9520  hashf1lem1  13277  seqcoll  13286  seqcoll2  13287  rlimcld2  14353  sumrblem  14486  fsumcvg  14487  fsumss  14500  incexclem  14612  prodrblem  14703  fprodcvg  14704  fprodss  14722  fprodn0f  14766  ruclem12  15014  coprmproddvdslem  15423  nnoddn2prmb  15565  prmreclem5  15671  ramub1lem1  15777  mreexd  16349  frgpnabllem1  18322  gsumzaddlem  18367  gsum2d  18417  dmdprdsplitlem  18482  pgpfac1lem2  18520  pgpfac1lem3  18522  irredrmul  18753  lsppratlem3  19197  lbsextlem4  19209  psgnodpmr  19984  frlmsslsp  20183  regsep2  21228  1stckgen  21405  regr1lem  21590  opnsubg  21958  zcld  22663  recld2  22664  bcthlem4  23170  iundisj  23362  iblss2  23617  itgeqa  23625  limcnlp  23687  dvloglem  24439  dvlog2lem  24443  ressatans  24706  regamcl  24832  facgam  24837  wilthlem2  24840  2lgslem2  25165  tgelrnln  25570  incistruhgr  26019  upgrres1  26250  usgr2pthlem  26715  iundisjf  29528  iundisjfi  29683  submateqlem1  30001  submateqlem2  30002  elzrhunit  30151  qqhval2  30154  esumrnmpt2  30258  inelpisys  30345  plymulx  30753  signstfvneq0  30777  noetalem3  31990  onint1  32573  lindsenlbs  33534  poimirlem23  33562  poimirlem30  33569  dvasin  33626  areacirclem4  33633  pridlc3  34002  rmspecsqrtnq  37787  rmspecsqrtnqOLD  37788  rmspecnonsq  37789  disjf1o  39692  difmap  39713  difmapsn  39718  supminfxr2  40012  icoiccdif  40068  iccdificc  40084  climrec  40153  limciccioolb  40171  limcrecl  40179  sumnnodd  40180  lptioo2  40181  lptioo1  40182  limcicciooub  40187  lptre2pt  40190  reclimc  40203  cnrefiisplem  40373  icccncfext  40418  fperdvper  40451  dvnmul  40476  itgcoscmulx  40503  itgsincmulx  40508  stoweidlem34  40569  stoweidlem39  40574  stoweidlem57  40592  wallispi  40605  stirlinglem8  40616  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem38  40680  fourierdlem40  40682  fourierdlem42  40684  fourierdlem46  40687  fourierdlem53  40694  fourierdlem56  40697  fourierdlem58  40699  fourierdlem62  40703  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  elaa2  40769  etransc  40818  gsumge0cl  40906  sge0fodjrnlem  40951  iundjiun  40995  meadjiunlem  41000  meaiininclem  41021  caragendifcl  41049  caratheodorylem1  41061  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem4  41133  hspdifhsp  41151  hspmbllem2  41162  preimagelt  41233  preimalegt  41234  dig1  42727
  Copyright terms: Public domain W3C validator