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

Theorem eldifn 3695
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 3550 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simprbi 479 1 (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1977  cdif 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543
This theorem is referenced by:  elndif  3696  noel  3878  disjel  3975  tz7.7  5666  funiunfv  6410  tfi  6945  peano5  6981  wfrlem10  7311  wfrlem13  7314  wfrlem16  7317  tz7.48-2  7424  tz7.49  7427  oaf1o  7530  undifixp  7830  domdifsn  7928  isinf  8058  ordtypelem7  8312  unxpwdom2  8376  inf3lem3  8410  infdifsn  8437  cantnfp1lem1  8458  cantnfp1lem3  8460  cantnflem1d  8468  setind  8493  fin23lem30  9047  domtriomlem  9147  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  ttukeylem7  9220  konigthlem  9269  fpwwe2lem13  9343  fpwwe2  9344  hashf1lem1  13096  rlimrecl  14159  sumrblem  14289  fsumcvg  14290  summolem2a  14293  fsumss  14303  sumss2  14304  binomlem  14400  isumltss  14419  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  fprodss  14517  fprodsplit  14535  fprodmodd  14567  sumodd  14949  prmreclem2  15459  prmreclem5  15462  ramub1lem1  15568  efgs1b  17972  gsumzsplit  18150  gsum2d  18194  gsum2d2lem  18195  dmdprdsplitlem  18259  pgpfac1lem1  18296  irredrmul  18530  lbsextlem2  18980  lbsextlem4  18982  psrlidm  19224  mplcoe1  19286  mplcoe5  19289  evlslem3  19335  evlslem1  19336  cnsubrg  19625  maducoeval2  20265  madugsum  20268  elcls  20687  isclo  20701  ptbasfi  21194  ptopn2  21197  xkopt  21268  kqdisj  21345  fin1aufil  21546  ptcmplem4  21669  opnsubg  21721  tsmssplit  21765  zcld  22424  recld2  22425  reconnlem1  22437  ioombl1lem4  23136  i1fima2sn  23253  itg1val2  23257  i1f0  23260  itg1addlem4  23272  mbfi1flim  23296  itg2splitlem  23321  itg2split  23322  itg2cnlem1  23334  itg2cnlem2  23335  itgss2  23385  itgeqa  23386  itgss3  23387  itgless  23389  ibladdlem  23392  itgaddlem1  23395  iblabslem  23400  itggt0  23414  itgcn  23415  ply1termlem  23763  plypf1  23772  plyaddlem1  23773  plymullem1  23774  coeeulem  23784  coeidlem  23797  coeid3  23800  coefv0  23808  coemulc  23815  dvply1  23843  vieta1lem2  23870  aaliou2  23899  logdmnrp  24187  regamcl  24587  lgam1  24590  gam1  24591  facgam  24592  chpub  24745  chebbnd1lem1  24958  strlem1  28493  partfun  28858  elzdif0  29352  indval2  29404  ind0  29409  sigaclfu2  29511  eulerpartlemb  29757  mrsubcn  30670  dfon2lem6  30937  ibladdnclem  32636  itgaddnclem1  32638  iblabsnclem  32643  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem8  32662  dvasin  32666  dvacos  32667  pridlc2  33041  pridlc3  33042  irrapx1  36410  pellqrex  36461  qirropth  36491  setindtr  36609  kelac1  36651  flcidc  36763  arearect  36820  areaquad  36821  mpct  38388  difmap  38394  difmapsn  38399  iccdificc  38613  fsumsupp0  38645  mccllem  38664  sumnnodd  38697  fprodcncf  38787  stoweidlem34  38927  stoweidlem44  38937  stirlinglem5  38971  fourierdlem62  39061  fouriersw  39124  elaa2lem  39126  etransclem44  39171  sge0iunmptlemfi  39306  sge0fodjrnlem  39309  iundjiunlem  39352  meadjiunlem  39358  isomenndlem  39420  hsphoidmvle2  39475  hsphoidmvle  39476  hspdifhsp  39506  hspmbllem2  39517  ovnsubadd2lem  39535  ovolval4lem1  39539  preimagelt  39589  preimalegt  39590
  Copyright terms: Public domain W3C validator