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

Theorem eldifn 3694
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 3549 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simprbi 478 1 (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1976  cdif 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542
This theorem is referenced by:  elndif  3695  noel  3877  disjel  3974  tz7.7  5652  funiunfv  6388  tfi  6922  peano5  6958  wfrlem10  7288  wfrlem13  7291  wfrlem16  7294  tz7.48-2  7401  tz7.49  7404  oaf1o  7507  undifixp  7807  domdifsn  7905  isinf  8035  ordtypelem7  8289  unxpwdom2  8353  inf3lem3  8387  infdifsn  8414  cantnfp1lem1  8435  cantnfp1lem3  8437  cantnflem1d  8445  setind  8470  fin23lem30  9024  domtriomlem  9124  axdc3lem4  9135  axdc4lem  9137  axcclem  9139  ttukeylem7  9197  konigthlem  9246  fpwwe2lem13  9320  fpwwe2  9321  hashf1lem1  13048  rlimrecl  14105  sumrblem  14235  fsumcvg  14236  summolem2a  14239  fsumss  14249  sumss2  14250  binomlem  14346  isumltss  14365  prodrblem  14444  fprodcvg  14445  prodmolem2a  14449  fprodss  14463  fprodsplit  14481  fprodmodd  14513  sumodd  14895  prmreclem2  15405  prmreclem5  15408  ramub1lem1  15514  efgs1b  17918  gsumzsplit  18096  gsum2d  18140  gsum2d2lem  18141  dmdprdsplitlem  18205  pgpfac1lem1  18242  irredrmul  18476  lbsextlem2  18926  lbsextlem4  18928  psrlidm  19170  mplcoe1  19232  mplcoe5  19235  evlslem3  19281  evlslem1  19282  cnsubrg  19571  maducoeval2  20207  madugsum  20210  elcls  20629  isclo  20643  ptbasfi  21136  ptopn2  21139  xkopt  21210  kqdisj  21287  fin1aufil  21488  ptcmplem4  21611  opnsubg  21663  tsmssplit  21707  zcld  22356  recld2  22357  reconnlem1  22369  ioombl1lem4  23053  i1fima2sn  23170  itg1val2  23174  i1f0  23177  itg1addlem4  23189  mbfi1flim  23213  itg2splitlem  23238  itg2split  23239  itg2cnlem1  23251  itg2cnlem2  23252  itgss2  23302  itgeqa  23303  itgss3  23304  itgless  23306  ibladdlem  23309  itgaddlem1  23312  iblabslem  23317  itggt0  23331  itgcn  23332  ply1termlem  23680  plypf1  23689  plyaddlem1  23690  plymullem1  23691  coeeulem  23701  coeidlem  23714  coeid3  23717  coefv0  23725  coemulc  23732  dvply1  23760  vieta1lem2  23787  aaliou2  23816  logdmnrp  24104  regamcl  24504  lgam1  24507  gam1  24508  facgam  24509  chpub  24662  chebbnd1lem1  24875  strlem1  28299  partfun  28664  elzdif0  29158  indval2  29210  ind0  29215  sigaclfu2  29317  eulerpartlemb  29563  mrsubcn  30476  dfon2lem6  30743  ibladdnclem  32432  itgaddnclem1  32434  iblabsnclem  32439  ftc1anclem5  32455  ftc1anclem6  32456  ftc1anclem8  32458  dvasin  32462  dvacos  32463  pridlc2  32837  pridlc3  32838  irrapx1  36206  pellqrex  36257  qirropth  36287  setindtr  36405  kelac1  36447  flcidc  36559  arearect  36616  areaquad  36617  mpct  38184  difmap  38190  difmapsn  38195  iccdificc  38410  fsumsupp0  38442  mccllem  38461  sumnnodd  38494  fprodcncf  38584  stoweidlem34  38724  stoweidlem44  38734  stirlinglem5  38768  fourierdlem62  38858  fouriersw  38921  elaa2lem  38923  etransclem44  38968  sge0iunmptlemfi  39103  sge0fodjrnlem  39106  iundjiunlem  39149  meadjiunlem  39155  isomenndlem  39217  hsphoidmvle2  39272  hsphoidmvle  39273  hspdifhsp  39303  hspmbllem2  39314  ovnsubadd2lem  39332  ovolval4lem1  39336  preimagelt  39386  preimalegt  39387
  Copyright terms: Public domain W3C validator