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

Theorem eldifd 3551
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3550. (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 3550 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
41, 2, 3sylanbrc 695 1 (𝜑𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1977  cdif 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543
This theorem is referenced by:  eqoreldif  4172  eqoreldifOLD  4173  xpdifid  5481  ressuppssdif  7203  oaf1o  7530  findcard2d  8087  cantnflem1  8469  cantnflem2  8470  fin23lem26  9030  isf34lem4  9082  isfin7-2  9101  axdc3lem4  9158  axdc4lem  9160  ttukeylem7  9220  pwfseqlem1  9359  pwfseqlem3  9361  hashf1lem1  13096  seqcoll  13105  seqcoll2  13106  rlimcld2  14157  sumrblem  14289  fsumcvg  14290  fsumss  14303  incexclem  14407  prodrblem  14498  fprodcvg  14499  fprodss  14517  fprodn0f  14561  ruclem12  14809  coprmproddvdslem  15214  nnoddn2prmb  15356  prmreclem5  15462  ramub1lem1  15568  mreexd  16125  frgpnabllem1  18099  gsumzaddlem  18144  gsum2d  18194  dmdprdsplitlem  18259  pgpfac1lem2  18297  pgpfac1lem3  18299  irredrmul  18530  lsppratlem3  18970  lbsextlem4  18982  psgnodpmr  19755  frlmsslsp  19954  regsep2  20990  1stckgen  21167  regr1lem  21352  opnsubg  21721  zcld  22424  recld2  22425  bcthlem4  22932  iundisj  23123  iblss2  23378  itgeqa  23386  limcnlp  23448  dvloglem  24194  dvlog2lem  24198  ressatans  24461  regamcl  24587  facgam  24592  wilthlem2  24595  2lgslem2  24920  tgelrnln  25325  incistruhgr  25746  nbcusgra  25992  usgrasscusgra  26011  uvtxnbgra  26021  frgrancvvdeqlem1  26557  frgrawopreglem4  26574  iundisjf  28784  iundisjfi  28942  submateqlem1  29201  submateqlem2  29202  elzrhunit  29351  qqhval2  29354  esumrnmpt2  29457  inelpisys  29544  plymulx  29951  signstfvneq0  29975  onint1  31618  lindsenlbs  32574  poimirlem23  32602  poimirlem30  32609  dvasin  32666  areacirclem4  32673  pridlc3  33042  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  rmspecnonsq  36490  disjf1o  38373  difmap  38394  difmapsn  38399  icoiccdif  38597  iccdificc  38613  climrec  38670  limciccioolb  38688  limcrecl  38696  sumnnodd  38697  lptioo2  38698  lptioo1  38699  limcicciooub  38704  lptre2pt  38707  reclimc  38720  icccncfext  38773  fperdvper  38808  dvnmul  38833  itgcoscmulx  38861  itgsincmulx  38866  stoweidlem34  38927  stoweidlem39  38932  stoweidlem57  38950  wallispi  38963  stirlinglem8  38974  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem38  39038  fourierdlem40  39040  fourierdlem42  39042  fourierdlem46  39045  fourierdlem53  39052  fourierdlem56  39055  fourierdlem58  39057  fourierdlem62  39061  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  elaa2  39127  etransc  39176  gsumge0cl  39264  sge0fodjrnlem  39309  iundjiun  39353  meadjiunlem  39358  meaiininclem  39376  caragendifcl  39404  caratheodorylem1  39416  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem4  39488  hspdifhsp  39506  hspmbllem2  39517  preimagelt  39589  preimalegt  39590  upgrres1  40532  usgr2pthlem  40969  frgrncvvdeqlem1  41469  frgrwopreglem4  41484  dig1  42200
  Copyright terms: Public domain W3C validator