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

Theorem eldifd 3546
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3545. (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 3545 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
41, 2, 3sylanbrc 694 1 (𝜑𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1975  cdif 3532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538
This theorem is referenced by:  eqoreldif  4167  eqoreldifOLD  4168  xpdifid  5463  ressuppssdif  7176  oaf1o  7503  findcard2d  8060  cantnflem1  8442  cantnflem2  8443  fin23lem26  9003  isf34lem4  9055  isfin7-2  9074  axdc3lem4  9131  axdc4lem  9133  ttukeylem7  9193  pwfseqlem1  9332  pwfseqlem3  9334  hashf1lem1  13044  seqcoll  13053  seqcoll2  13054  rlimcld2  14099  sumrblem  14231  fsumcvg  14232  fsumss  14245  incexclem  14349  prodrblem  14440  fprodcvg  14441  fprodss  14459  fprodn0f  14503  ruclem12  14751  coprmproddvdslem  15156  nnoddn2prmb  15298  prmreclem5  15404  ramub1lem1  15510  mreexd  16067  frgpnabllem1  18041  gsumzaddlem  18086  gsum2d  18136  dmdprdsplitlem  18201  pgpfac1lem2  18239  pgpfac1lem3  18241  irredrmul  18472  lsppratlem3  18912  lbsextlem4  18924  psgnodpmr  19696  frlmsslsp  19892  regsep2  20928  1stckgen  21105  regr1lem  21290  opnsubg  21659  zcld  22352  recld2  22353  bcthlem4  22845  iundisj  23036  iblss2  23291  itgeqa  23299  limcnlp  23361  dvloglem  24107  dvlog2lem  24111  ressatans  24374  regamcl  24500  facgam  24505  wilthlem2  24508  2lgslem2  24833  tgelrnln  25239  nbcusgra  25754  usgrasscusgra  25773  uvtxnbgra  25783  frgrancvvdeqlem1  26319  frgrawopreglem4  26336  iundisjf  28586  iundisjfi  28744  submateqlem1  29003  submateqlem2  29004  elzrhunit  29153  qqhval2  29156  esumrnmpt2  29259  inelpisys  29346  plymulx  29753  signstfvneq0  29777  onint1  31420  lindsenlbs  32373  poimirlem23  32401  poimirlem30  32408  dvasin  32465  areacirclem4  32472  pridlc3  32841  rmspecsqrtnq  36287  rmspecsqrtnqOLD  36288  rmspecnonsq  36289  disjf1o  38172  difmap  38193  difmapsn  38198  icoiccdif  38397  iccdificc  38413  climrec  38470  limciccioolb  38488  limcrecl  38496  sumnnodd  38497  lptioo2  38498  lptioo1  38499  limcicciooub  38504  lptre2pt  38507  reclimc  38520  icccncfext  38573  fperdvper  38608  dvnmul  38633  itgcoscmulx  38661  itgsincmulx  38666  stoweidlem34  38727  stoweidlem39  38732  stoweidlem57  38750  wallispi  38763  stirlinglem8  38774  dirkercncflem2  38797  dirkercncflem4  38799  fourierdlem38  38838  fourierdlem40  38840  fourierdlem42  38842  fourierdlem46  38845  fourierdlem53  38852  fourierdlem56  38855  fourierdlem58  38857  fourierdlem62  38861  fourierdlem74  38873  fourierdlem75  38874  fourierdlem76  38875  fourierdlem78  38877  fourierdlem93  38892  fourierdlem103  38902  fourierdlem104  38903  fouriersw  38924  elaa2  38927  etransc  38976  gsumge0cl  39064  sge0fodjrnlem  39109  iundjiun  39153  meadjiunlem  39158  meaiininclem  39176  caragendifcl  39204  caratheodorylem1  39216  hoidmvlelem1  39285  hoidmvlelem2  39286  hoidmvlelem4  39288  hspdifhsp  39306  hspmbllem2  39317  preimagelt  39389  preimalegt  39390  incistruhgr  40303  upgrres1  40530  usgr2pthlem  40967  frgrncvvdeqlem1  41467  frgrwopreglem4  41482  dig1  42198
  Copyright terms: Public domain W3C validator