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

Theorem eldifn 3943
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 3790 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simprbi 486 1 (𝐴 ∈ (𝐵𝐶) → ¬ 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2157  cdif 3777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-dif 3783
This theorem is referenced by:  elndif  3944  noel  4131  disjel  4232  tz7.7  5976  funiunfv  6740  tfi  7293  peano5  7329  wfrlem10  7670  wfrlem13  7673  wfrlem16  7676  tz7.48-2  7783  tz7.49  7786  oaf1o  7890  undifixp  8191  domdifsn  8292  isinf  8422  ordtypelem7  8678  unxpwdom2  8742  inf3lem3  8784  infdifsn  8811  cantnfp1lem1  8832  cantnfp1lem3  8834  cantnflem1d  8842  setind  8867  fin23lem30  9459  domtriomlem  9559  axdc3lem4  9570  axdc4lem  9572  axcclem  9574  ttukeylem7  9632  konigthlem  9685  fpwwe2lem13  9759  fpwwe2  9760  hashf1lem1  13476  rlimrecl  14554  sumrblem  14685  fsumcvg  14686  summolem2a  14689  fsumss  14699  sumss2  14700  binomlem  14803  isumltss  14822  prodrblem  14900  fprodcvg  14901  prodmolem2a  14905  fprodss  14919  fprodsplit  14937  fprodmodd  14968  sumodd  15351  prmreclem2  15858  prmreclem5  15861  ramub1lem1  15967  efgs1b  18370  gsumzsplit  18548  gsum2d  18592  gsum2d2lem  18593  dmdprdsplitlem  18658  pgpfac1lem1  18695  irredrmul  18929  lbsextlem2  19388  lbsextlem4  19390  psrlidm  19632  mplcoe1  19694  mplcoe5  19697  evlslem3  19742  evlslem1  19743  cnsubrg  20034  maducoeval2  20678  madugsum  20681  elcls  21112  isclo  21126  ptbasfi  21619  ptopn2  21622  xkopt  21693  kqdisj  21770  fin1aufil  21970  ptcmplem4  22093  opnsubg  22145  tsmssplit  22189  zcld  22850  recld2  22851  reconnlem1  22863  ioombl1lem4  23565  i1fima2sn  23684  itg1val2  23688  i1f0  23691  itg1addlem4  23703  mbfi1flim  23727  itg2splitlem  23752  itg2split  23753  itg2cnlem1  23765  itg2cnlem2  23766  itgss2  23816  itgeqa  23817  itgss3  23818  itgless  23820  ibladdlem  23823  itgaddlem1  23826  iblabslem  23831  itggt0  23845  itgcn  23846  ply1termlem  24196  plypf1  24205  plyaddlem1  24206  plymullem1  24207  coeeulem  24217  coeidlem  24230  coeid3  24233  coefv0  24241  coemulc  24248  dvply1  24276  vieta1lem2  24303  aaliou2  24332  logdmnrp  24624  regamcl  25024  lgam1  25027  gam1  25028  facgam  25029  chpub  25182  chebbnd1lem1  25395  numedglnl  26277  strlem1  29460  partfun  29825  elzdif0  30372  indval2  30424  ind0  30428  sigaclfu2  30532  eulerpartlemb  30778  mrsubcn  31761  dfon2lem6  32035  ibladdnclem  33797  itgaddnclem1  33799  iblabsnclem  33804  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem8  33823  dvasin  33827  dvacos  33828  pridlc2  34201  pridlc3  34202  irrapx1  37912  pellqrex  37963  qirropth  37992  setindtr  38110  kelac1  38152  flcidc  38263  arearect  38319  areaquad  38320  mpct  39898  difmap  39904  difmapsn  39909  iccdificc  40264  fsumsupp0  40308  mccllem  40327  sumnnodd  40360  fprodcncf  40612  stoweidlem34  40748  stoweidlem44  40758  stirlinglem5  40792  fourierdlem62  40882  fouriersw  40945  elaa2lem  40947  etransclem44  40992  sge0iunmptlemfi  41127  sge0fodjrnlem  41130  iundjiunlem  41173  meadjiunlem  41179  isomenndlem  41244  hsphoidmvle2  41299  hsphoidmvle  41300  hspdifhsp  41330  hspmbllem2  41341  ovnsubadd2lem  41359  ovolval4lem1  41363  preimagelt  41412  preimalegt  41413
  Copyright terms: Public domain W3C validator