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

Theorem eldifn 3766
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 3617 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simprbi 479 1 (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2030  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610
This theorem is referenced by:  elndif  3767  noel  3952  disjel  4056  tz7.7  5787  funiunfv  6546  tfi  7095  peano5  7131  wfrlem10  7469  wfrlem13  7472  wfrlem16  7475  tz7.48-2  7582  tz7.49  7585  oaf1o  7688  undifixp  7986  domdifsn  8084  isinf  8214  ordtypelem7  8470  unxpwdom2  8534  inf3lem3  8565  infdifsn  8592  cantnfp1lem1  8613  cantnfp1lem3  8615  cantnflem1d  8623  setind  8648  fin23lem30  9202  domtriomlem  9302  axdc3lem4  9313  axdc4lem  9315  axcclem  9317  ttukeylem7  9375  konigthlem  9428  fpwwe2lem13  9502  fpwwe2  9503  hashf1lem1  13277  rlimrecl  14355  sumrblem  14486  fsumcvg  14487  summolem2a  14490  fsumss  14500  sumss2  14501  binomlem  14605  isumltss  14624  prodrblem  14703  fprodcvg  14704  prodmolem2a  14708  fprodss  14722  fprodsplit  14740  fprodmodd  14772  sumodd  15158  prmreclem2  15668  prmreclem5  15671  ramub1lem1  15777  efgs1b  18195  gsumzsplit  18373  gsum2d  18417  gsum2d2lem  18418  dmdprdsplitlem  18482  pgpfac1lem1  18519  irredrmul  18753  lbsextlem2  19207  lbsextlem4  19209  psrlidm  19451  mplcoe1  19513  mplcoe5  19516  evlslem3  19562  evlslem1  19563  cnsubrg  19854  maducoeval2  20494  madugsum  20497  elcls  20925  isclo  20939  ptbasfi  21432  ptopn2  21435  xkopt  21506  kqdisj  21583  fin1aufil  21783  ptcmplem4  21906  opnsubg  21958  tsmssplit  22002  zcld  22663  recld2  22664  reconnlem1  22676  ioombl1lem4  23375  i1fima2sn  23492  itg1val2  23496  i1f0  23499  itg1addlem4  23511  mbfi1flim  23535  itg2splitlem  23560  itg2split  23561  itg2cnlem1  23573  itg2cnlem2  23574  itgss2  23624  itgeqa  23625  itgss3  23626  itgless  23628  ibladdlem  23631  itgaddlem1  23634  iblabslem  23639  itggt0  23653  itgcn  23654  ply1termlem  24004  plypf1  24013  plyaddlem1  24014  plymullem1  24015  coeeulem  24025  coeidlem  24038  coeid3  24041  coefv0  24049  coemulc  24056  dvply1  24084  vieta1lem2  24111  aaliou2  24140  logdmnrp  24432  regamcl  24832  lgam1  24835  gam1  24836  facgam  24837  chpub  24990  chebbnd1lem1  25203  numedglnl  26084  strlem1  29237  partfun  29603  elzdif0  30152  indval2  30204  ind0  30208  sigaclfu2  30312  eulerpartlemb  30558  mrsubcn  31542  dfon2lem6  31817  ibladdnclem  33596  itgaddnclem1  33598  iblabsnclem  33603  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem8  33622  dvasin  33626  dvacos  33627  pridlc2  34001  pridlc3  34002  irrapx1  37709  pellqrex  37760  qirropth  37790  setindtr  37908  kelac1  37950  flcidc  38061  arearect  38118  areaquad  38119  mpct  39707  difmap  39713  difmapsn  39718  iccdificc  40084  fsumsupp0  40128  mccllem  40147  sumnnodd  40180  fprodcncf  40432  stoweidlem34  40569  stoweidlem44  40579  stirlinglem5  40613  fourierdlem62  40703  fouriersw  40766  elaa2lem  40768  etransclem44  40813  sge0iunmptlemfi  40948  sge0fodjrnlem  40951  iundjiunlem  40994  meadjiunlem  41000  isomenndlem  41065  hsphoidmvle2  41120  hsphoidmvle  41121  hspdifhsp  41151  hspmbllem2  41162  ovnsubadd2lem  41180  ovolval4lem1  41184  preimagelt  41233  preimalegt  41234
  Copyright terms: Public domain W3C validator