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

Theorem eldifd 3921
 Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3920. (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 3920 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
41, 2, 3sylanbrc 586 1 (𝜑𝐴 ∈ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2115   ∖ cdif 3907 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-dif 3913 This theorem is referenced by:  rexdifi  4098  eqoreldif  4595  xpdifid  5998  funeldmdif  7722  ressuppssdif  7826  oaf1o  8164  findcard2d  8736  cantnflem1  9128  cantnflem2  9129  fin23lem26  9724  isf34lem4  9776  isfin7-2  9795  axdc3lem4  9852  axdc4lem  9854  ttukeylem7  9914  pwfseqlem1  10057  pwfseqlem3  10059  hashf1lem1  13797  seqcoll  13806  seqcoll2  13807  rlimcld2  14914  sumrblem  15047  fsumcvg  15048  fsumss  15061  incexclem  15170  prodrblem  15262  fprodcvg  15263  fprodss  15281  fprodn0f  15324  ruclem12  15573  sqrt2irr0  15583  coprmproddvdslem  15983  nnoddn2prmb  16127  prmreclem5  16233  ramub1lem1  16339  mreexd  16891  frgpnabllem1  18971  gsumzaddlem  19019  gsum2d  19070  gsumxp2  19078  dmdprdsplitlem  19137  pgpfac1lem2  19175  pgpfac1lem3  19177  irredrmul  19435  lsppratlem3  19896  lbsextlem4  19908  psgnodpmr  20709  frlmsslsp  20915  regsep2  21959  1stckgen  22137  regr1lem  22322  opnsubg  22691  zcld  23396  recld2  23397  bcthlem4  23909  iundisj  24130  iblss2  24387  itgeqa  24395  limcnlp  24459  dvloglem  25217  dvlog2lem  25221  2irrexpq  25299  logbgcd1irr  25358  ressatans  25498  regamcl  25624  facgam  25629  wilthlem2  25632  2lgslem2  25957  tgelrnln  26402  incistruhgr  26850  upgrres1  27081  usgr2pthlem  27530  iundisjf  30325  iundisjfi  30505  cycpmfv3  30764  cyc3conja  30806  submateqlem1  31082  submateqlem2  31083  elzrhunit  31227  qqhval2  31230  esumrnmpt2  31334  inelpisys  31420  plymulx  31825  noetalem3  33226  onint1  33804  lindsadd  34928  lindsenlbs  34930  poimirlem23  34958  poimirlem30  34965  dvasin  35019  areacirclem4  35026  pridlc3  35389  nelsubginvcld  39242  nelsubgcld  39243  rtprmirr  39316  prjspersym  39396  prjspreln0  39398  prjspvs  39399  rmspecsqrtnq  39642  rmspecnonsq  39643  pr2eldif1  40048  pr2eldif2  40049  disjf1o  41606  difmap  41624  difmapsn  41629  supminfxr2  41899  icoiccdif  41952  iccdificc  41967  climrec  42036  limciccioolb  42054  limcrecl  42062  sumnnodd  42063  lptioo2  42064  lptioo1  42065  limcicciooub  42070  lptre2pt  42073  reclimc  42086  cnrefiisplem  42262  icccncfext  42320  fperdvper  42352  dvnmul  42376  itgcoscmulx  42402  itgsincmulx  42407  stoweidlem34  42467  stoweidlem39  42472  stoweidlem57  42490  wallispi  42503  stirlinglem8  42514  dirkercncflem2  42537  dirkercncflem4  42539  fourierdlem38  42578  fourierdlem40  42580  fourierdlem42  42582  fourierdlem46  42585  fourierdlem53  42592  fourierdlem56  42595  fourierdlem58  42597  fourierdlem62  42601  fourierdlem74  42613  fourierdlem75  42614  fourierdlem76  42615  fourierdlem78  42617  fourierdlem93  42632  fourierdlem103  42642  fourierdlem104  42643  fouriersw  42664  elaa2  42667  etransc  42716  gsumge0cl  42801  sge0fodjrnlem  42846  iundjiun  42890  meadjiunlem  42895  meaiininclem  42916  caragendifcl  42944  caratheodorylem1  42956  hoidmvlelem1  43025  hoidmvlelem2  43026  hoidmvlelem4  43028  hspdifhsp  43046  hspmbllem2  43057  preimagelt  43128  preimalegt  43129  sqrtnegnre  43655  requad01  43931  dig1  44813
 Copyright terms: Public domain W3C validator