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

Theorem eldifn 4088
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 3921 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simprbi 498 1 (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  cdif 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-dif 3914
This theorem is referenced by:  elndif  4089  disjel  4417  tz7.7  6344  partfun  6649  funiunfv  7196  tfi  7790  peano5  7831  peano5OLD  7832  frrlem11  8228  frrlem12  8229  frrlem14  8231  wfrlem10OLD  8265  wfrlem13OLD  8268  wfrlem16OLD  8271  tz7.48-2  8389  tz7.49  8392  oaf1o  8511  undifixp  8873  domdifsn  8999  isinf  9205  isinfOLD  9206  ordtypelem7  9461  unxpwdom2  9525  inf3lem3  9567  infdifsn  9594  cantnfp1lem1  9615  cantnfp1lem3  9617  cantnflem1d  9625  setind  9671  fin23lem30  10279  domtriomlem  10379  axdc3lem4  10390  axdc4lem  10392  axcclem  10394  ttukeylem7  10452  konigthlem  10505  fpwwe2lem12  10579  fpwwe2  10580  hashf1lem1  14354  hashf1lem1OLD  14355  rlimrecl  15463  sumrblem  15597  fsumcvg  15598  summolem2a  15601  fsumss  15611  sumss2  15612  binomlem  15715  isumltss  15734  prodrblem  15813  fprodcvg  15814  prodmolem2a  15818  fprodss  15832  fprodsplit  15850  fprodmodd  15881  sumodd  16271  prmreclem2  16790  prmreclem5  16793  ramub1lem1  16899  efgs1b  19519  gsumzsplit  19705  gsum2d  19750  gsum2d2lem  19751  dmdprdsplitlem  19817  pgpfac1lem1  19854  irredrmul  20137  lbsextlem2  20623  lbsextlem4  20625  cnsubrg  20860  psrlidm  21375  mplcoe1  21441  mplcoe5  21444  evlslem3  21493  maducoeval2  21992  madugsum  21995  elcls  22427  isclo  22441  ptbasfi  22935  ptopn2  22938  xkopt  23009  kqdisj  23086  fin1aufil  23286  ptcmplem4  23409  opnsubg  23462  tsmssplit  23506  zcld  24179  recld2  24180  reconnlem1  24192  ioombl1lem4  24928  i1fima2sn  25047  itg1val2  25051  i1f0  25054  itg1addlem4  25066  itg1addlem4OLD  25067  mbfi1flim  25091  itg2splitlem  25116  itg2split  25117  itg2cnlem1  25129  itg2cnlem2  25130  itgss2  25180  itgeqa  25181  itgss3  25182  itgless  25184  ibladdlem  25187  itgaddlem1  25190  iblabslem  25195  itggt0  25211  itgcn  25212  ply1termlem  25567  plypf1  25576  plyaddlem1  25577  plymullem1  25578  coeeulem  25588  coeidlem  25601  coeid3  25604  coefv0  25612  coemulc  25619  dvply1  25647  vieta1lem2  25674  aaliou2  25703  logdmnrp  25999  regamcl  26413  lgam1  26416  gam1  26417  facgam  26418  chpub  26571  chebbnd1lem1  26820  numedglnl  28098  strlem1  31195  cycpmco2  31985  indval2  32616  ind0  32620  sigaclfu2  32723  eulerpartlemb  32971  mrsubcn  34116  dfon2lem6  34366  lindsadd  36074  ibladdnclem  36137  itgaddnclem1  36139  iblabsnclem  36144  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem8  36161  dvasin  36165  dvacos  36166  pridlc2  36534  pridlc3  36535  fsuppssind  40771  irrapx1  41154  pellqrex  41205  qirropth  41234  setindtr  41351  kelac1  41393  flcidc  41504  arearect  41552  areaquad  41553  cantnfub  41658  mpct  43429  difmap  43435  difmapsn  43440  iccdificc  43784  fsumsupp0  43826  mccllem  43845  sumnnodd  43878  fprodcncf  44148  stoweidlem34  44282  stoweidlem44  44292  stirlinglem5  44326  fourierdlem62  44416  fouriersw  44479  elaa2lem  44481  etransclem44  44526  sge0iunmptlemfi  44661  sge0fodjrnlem  44664  meadjiunlem  44713  isomenndlem  44778  hsphoidmvle2  44833  hsphoidmvle  44834  hspdifhsp  44864  hspmbllem2  44875  ovnsubadd2lem  44893  ovolval4lem1  44897  preimagelt  44947  preimalegt  44948
  Copyright terms: Public domain W3C validator