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

Theorem eldifn 3876
Description: Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
Assertion
Ref Expression
eldifn (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)

Proof of Theorem eldifn
StepHypRef Expression
1 eldif 3725 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simprbi 483 1 (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2139  cdif 3712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718
This theorem is referenced by:  elndif  3877  noel  4062  disjel  4167  tz7.7  5910  funiunfv  6670  tfi  7219  peano5  7255  wfrlem10  7594  wfrlem13  7597  wfrlem16  7600  tz7.48-2  7707  tz7.49  7710  oaf1o  7814  undifixp  8112  domdifsn  8210  isinf  8340  ordtypelem7  8596  unxpwdom2  8660  inf3lem3  8702  infdifsn  8729  cantnfp1lem1  8750  cantnfp1lem3  8752  cantnflem1d  8760  setind  8785  fin23lem30  9376  domtriomlem  9476  axdc3lem4  9487  axdc4lem  9489  axcclem  9491  ttukeylem7  9549  konigthlem  9602  fpwwe2lem13  9676  fpwwe2  9677  hashf1lem1  13451  rlimrecl  14530  sumrblem  14661  fsumcvg  14662  summolem2a  14665  fsumss  14675  sumss2  14676  binomlem  14780  isumltss  14799  prodrblem  14878  fprodcvg  14879  prodmolem2a  14883  fprodss  14897  fprodsplit  14915  fprodmodd  14947  sumodd  15333  prmreclem2  15843  prmreclem5  15846  ramub1lem1  15952  efgs1b  18369  gsumzsplit  18547  gsum2d  18591  gsum2d2lem  18592  dmdprdsplitlem  18656  pgpfac1lem1  18693  irredrmul  18927  lbsextlem2  19381  lbsextlem4  19383  psrlidm  19625  mplcoe1  19687  mplcoe5  19690  evlslem3  19736  evlslem1  19737  cnsubrg  20028  maducoeval2  20668  madugsum  20671  elcls  21099  isclo  21113  ptbasfi  21606  ptopn2  21609  xkopt  21680  kqdisj  21757  fin1aufil  21957  ptcmplem4  22080  opnsubg  22132  tsmssplit  22176  zcld  22837  recld2  22838  reconnlem1  22850  ioombl1lem4  23549  i1fima2sn  23666  itg1val2  23670  i1f0  23673  itg1addlem4  23685  mbfi1flim  23709  itg2splitlem  23734  itg2split  23735  itg2cnlem1  23747  itg2cnlem2  23748  itgss2  23798  itgeqa  23799  itgss3  23800  itgless  23802  ibladdlem  23805  itgaddlem1  23808  iblabslem  23813  itggt0  23827  itgcn  23828  ply1termlem  24178  plypf1  24187  plyaddlem1  24188  plymullem1  24189  coeeulem  24199  coeidlem  24212  coeid3  24215  coefv0  24223  coemulc  24230  dvply1  24258  vieta1lem2  24285  aaliou2  24314  logdmnrp  24607  regamcl  25007  lgam1  25010  gam1  25011  facgam  25012  chpub  25165  chebbnd1lem1  25378  numedglnl  26259  strlem1  29439  partfun  29805  elzdif0  30354  indval2  30406  ind0  30410  sigaclfu2  30514  eulerpartlemb  30760  mrsubcn  31744  dfon2lem6  32019  ibladdnclem  33797  itgaddnclem1  33799  iblabsnclem  33804  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem8  33823  dvasin  33827  dvacos  33828  pridlc2  34202  pridlc3  34203  irrapx1  37912  pellqrex  37963  qirropth  37993  setindtr  38111  kelac1  38153  flcidc  38264  arearect  38321  areaquad  38322  mpct  39910  difmap  39916  difmapsn  39921  iccdificc  40287  fsumsupp0  40331  mccllem  40350  sumnnodd  40383  fprodcncf  40635  stoweidlem34  40772  stoweidlem44  40782  stirlinglem5  40816  fourierdlem62  40906  fouriersw  40969  elaa2lem  40971  etransclem44  41016  sge0iunmptlemfi  41151  sge0fodjrnlem  41154  iundjiunlem  41197  meadjiunlem  41203  isomenndlem  41268  hsphoidmvle2  41323  hsphoidmvle  41324  hspdifhsp  41354  hspmbllem2  41365  ovnsubadd2lem  41383  ovolval4lem1  41387  preimagelt  41436  preimalegt  41437
  Copyright terms: Public domain W3C validator