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

Theorem eldifn 4108
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 3950 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simprbi 497 1 (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  cdif 3937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943
This theorem is referenced by:  elndif  4109  noelOLD  4301  disjel  4409  tz7.7  6215  funiunfv  7001  tfi  7556  peano5  7593  wfrlem10  7955  wfrlem13  7958  wfrlem16  7961  tz7.48-2  8069  tz7.49  8072  oaf1o  8179  undifixp  8487  domdifsn  8589  isinf  8720  ordtypelem7  8977  unxpwdom2  9041  inf3lem3  9082  infdifsn  9109  cantnfp1lem1  9130  cantnfp1lem3  9132  cantnflem1d  9140  setind  9165  fin23lem30  9753  domtriomlem  9853  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  ttukeylem7  9926  konigthlem  9979  fpwwe2lem13  10053  fpwwe2  10054  hashf1lem1  13803  rlimrecl  14927  sumrblem  15058  fsumcvg  15059  summolem2a  15062  fsumss  15072  sumss2  15073  binomlem  15174  isumltss  15193  prodrblem  15273  fprodcvg  15274  prodmolem2a  15278  fprodss  15292  fprodsplit  15310  fprodmodd  15341  sumodd  15729  prmreclem2  16243  prmreclem5  16246  ramub1lem1  16352  efgs1b  18782  gsumzsplit  18967  gsum2d  19012  gsum2d2lem  19013  dmdprdsplitlem  19079  pgpfac1lem1  19116  irredrmul  19377  lbsextlem2  19851  lbsextlem4  19853  psrlidm  20102  mplcoe1  20164  mplcoe5  20167  evlslem3  20211  cnsubrg  20521  maducoeval2  21165  madugsum  21168  elcls  21597  isclo  21611  ptbasfi  22105  ptopn2  22108  xkopt  22179  kqdisj  22256  fin1aufil  22456  ptcmplem4  22579  opnsubg  22631  tsmssplit  22675  zcld  23336  recld2  23337  reconnlem1  23349  ioombl1lem4  24077  i1fima2sn  24196  itg1val2  24200  i1f0  24203  itg1addlem4  24215  mbfi1flim  24239  itg2splitlem  24264  itg2split  24265  itg2cnlem1  24277  itg2cnlem2  24278  itgss2  24328  itgeqa  24329  itgss3  24330  itgless  24332  ibladdlem  24335  itgaddlem1  24338  iblabslem  24343  itggt0  24357  itgcn  24358  ply1termlem  24708  plypf1  24717  plyaddlem1  24718  plymullem1  24719  coeeulem  24729  coeidlem  24742  coeid3  24745  coefv0  24753  coemulc  24760  dvply1  24788  vieta1lem2  24815  aaliou2  24844  logdmnrp  25137  regamcl  25552  lgam1  25555  gam1  25556  facgam  25557  chpub  25710  chebbnd1lem1  25959  numedglnl  26843  strlem1  29941  partfun  30336  cycpmco2  30689  indval2  31159  ind0  31163  sigaclfu2  31266  eulerpartlemb  31512  mrsubcn  32650  dfon2lem6  32917  frrlem11  33017  frrlem12  33018  frrlem14  33020  lindsadd  34752  ibladdnclem  34815  itgaddnclem1  34817  iblabsnclem  34822  ftc1anclem5  34838  ftc1anclem6  34839  ftc1anclem8  34841  dvasin  34845  dvacos  34846  pridlc2  35218  pridlc3  35219  irrapx1  39290  pellqrex  39341  qirropth  39370  setindtr  39486  kelac1  39528  flcidc  39639  arearect  39687  areaquad  39688  mpct  41329  difmap  41335  difmapsn  41340  iccdificc  41680  fsumsupp0  41724  mccllem  41743  sumnnodd  41776  fprodcncf  42049  stoweidlem34  42185  stoweidlem44  42195  stirlinglem5  42229  fourierdlem62  42319  fouriersw  42382  elaa2lem  42384  etransclem44  42429  sge0iunmptlemfi  42561  sge0fodjrnlem  42564  iundjiunlem  42607  meadjiunlem  42613  isomenndlem  42678  hsphoidmvle2  42733  hsphoidmvle  42734  hspdifhsp  42764  hspmbllem2  42775  ovnsubadd2lem  42793  ovolval4lem1  42797  preimagelt  42846  preimalegt  42847
  Copyright terms: Public domain W3C validator