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

Theorem eldifi 3875
Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldifi (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)

Proof of Theorem eldifi
StepHypRef Expression
1 eldif 3725 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 478 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2139  cdif 3712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718
This theorem is referenced by:  difss  3880  noel  4062  eqoreldif  4369  eqoreldifOLD  4370  xpdifid  5720  tz7.7  5910  tfi  7218  peano5  7254  wfrlem10  7593  wfrlem15  7598  tz7.48-1  7707  tz7.49  7709  dif20el  7754  oaf1o  7812  oeordi  7836  oeord  7837  oecan  7838  oeword  7839  oeworde  7842  oelimcl  7849  oeeulem  7850  oeeui  7851  oaabs2  7894  boxcutc  8117  domdifsn  8208  isinf  8338  pssnn  8343  pwfilem  8425  fsuppco2  8473  fsuppcor  8474  ordtypelem7  8594  unxpwdom2  8658  inf3lem3  8700  cantnfp1lem1  8748  cantnfp1lem3  8750  infxpenc2lem1  9032  dfacacn  9155  isf32lem3  9369  isf34lem4  9391  fin67  9409  isfin7-2  9410  domtriomlem  9456  axdc2lem  9462  axdc3lem4  9467  axdc4lem  9469  ttukeylem7  9529  konigthlem  9582  fpwwe2lem13  9656  fpwwe2  9657  modfzo0difsn  12936  hashf1lem1  13431  hashle2prv  13452  rlimrege0  14509  rlimrecl  14510  sumrblem  14641  fsumcvg  14642  summolem2a  14645  fsumss  14655  fsumless  14727  cvgcmpce  14749  binomlem  14760  incexclem  14767  incexc  14768  isumltss  14779  prodrblem  14858  fprodcvg  14859  prodmolem2a  14863  fprodss  14877  fprodn0f  14921  fprodeq0g  14924  fprodmodd  14927  rpnnen2lem10  15151  rpnnen2lem11  15152  sumeven  15312  sumodd  15313  lcmfunsnlem2  15555  oddprmge3  15614  oddprm  15717  nnoddn2prm  15718  nnoddn2prmb  15720  iserodd  15742  prmreclem2  15823  prmreclem3  15824  prmreclem5  15826  4sqlem19  15869  prmdvdsprmo  15948  prmodvdslcmf  15953  prmlem0  16014  firest  16295  grpinvnzcl  17688  symgextfv  18038  pmtrf  18075  pmtrdifellem3  18098  sylow2alem2  18233  sylow2a  18234  efgsf  18342  efgsrel  18347  efgs1  18348  efgsfo  18352  efgredlemc  18358  gsumzaddlem  18521  gsumzadd  18522  gsumzmhm  18537  gsum2d2lem  18572  dprdfadd  18619  dprdres  18627  subgdmdprd  18633  dmdprdsplitlem  18636  dmdprdsplit2lem  18644  dpjidcl  18657  ablfac1b  18669  pgpfac1lem1  18673  gsummgp0  18808  isirred  18899  irredrmul  18907  isdrng2  18959  isdrngd  18974  lcomfsupp  19105  lbspropd  19301  lspsneq  19324  lsppratlem6  19354  lbsextlem2  19361  lbsextlem4  19363  ringelnzr  19468  psrbaglesupp  19570  psrlidm  19605  psrridm  19606  mplsubglem  19636  mpllsslem  19637  mplsubrglem  19641  mplmonmul  19666  mplcoe1  19667  mplcoe5  19670  mplbas2  19672  evlslem3  19716  coe1tmmul2  19848  coe1tmmul  19849  xrs1mnd  19986  xrs10  19987  xrs1cmn  19988  cnsubrg  20008  psgnodpm  20136  zrhpsgnodpm  20140  evpmodpmf1o  20144  uvcresum  20334  frlmssuvc1  20335  frlmsslsp  20337  frlmup2  20340  lindfrn  20362  f1lindf  20363  lindfmm  20368  islindf4  20379  dmatmul  20505  1marepvsma1  20591  mdetdiaglem  20606  mdetrlin  20610  mdetrsca  20611  mdetralt  20616  maducoeval2  20648  madugsum  20651  symgmatr01  20662  gsummatr01lem3  20665  gsummatr01lem4  20666  gsummatr01  20667  smadiadetlem0  20669  smadiadetlem1a  20671  cmpfi  21413  2ndcdisj2  21462  elptr2  21579  ptcnplem  21626  xkopt  21660  kqdisj  21737  fin1aufil  21937  ptcmplem2  22058  ptcmplem3  22059  ptcmplem4  22060  opnsubg  22112  lpbl  22509  blcld  22511  zcld  22817  recld2  22818  reconnlem1  22830  divcn  22872  iundisj  23516  mbfeqalem  23608  itg1val2  23650  itg1ge0  23652  i1fmullem  23660  i1fadd  23661  itg1addlem4  23665  itg1mulc  23670  itg1lea  23678  itg1le  23679  mbfi1fseqlem4  23684  itg2uba  23709  itg2lea  23710  itg2eqa  23711  itg2splitlem  23714  itg2split  23715  itgeqa  23779  ellimc3  23842  dvaddbr  23900  dvmulbr  23901  dvcobr  23908  dvcjbr  23911  dvrec  23917  dvrecg  23935  dvcnvlem  23938  dvexp3  23940  dveflem  23941  tdeglem4  24019  deg1n0ima  24048  deg1mul3le  24075  ig1peu  24130  ply1termlem  24158  plypf1  24167  plyaddlem1  24168  plymullem1  24169  coeeulem  24179  coeidlem  24192  coeid3  24195  coefv0  24203  coemulhi  24209  coemulc  24210  dvply1  24238  fta1  24262  vieta1lem2  24265  elaa  24270  elqaalem2  24274  aannenlem2  24283  aaliou2  24294  tayl0  24315  dvtaylp  24323  taylthlem1  24326  taylthlem2  24327  pserdvlem2  24381  logbcl  24704  relogbreexp  24712  relogbcxp  24722  cxplogb  24723  dcubic  24772  rlimcnp  24891  jensen  24914  dmgmaddn0  24948  dmlogdmgm  24949  lgamgulmlem2  24955  igamz  24973  gamp1  24983  regamcl  24986  wilthlem2  24994  basellem3  25008  chpub  25144  logexprlim  25149  lgslem1  25221  lgslem4  25224  lgsvalmod  25240  lgsqr  25275  lgsqrmod  25276  lgsqrmodndvds  25277  gausslemma2dlem0b  25281  gausslemma2dlem0c  25282  gausslemma2dlem0i  25288  gausslemma2dlem1a  25289  gausslemma2dlem4  25293  gausslemma2dlem5a  25294  gausslemma2dlem7  25297  gausslemma2d  25298  lgsquadlem1  25304  lgsquad2  25310  m1lgs  25312  2lgsoddprm  25340  dchrisum0fno1  25399  rplogsum  25415  ishpg  25850  umgrislfupgrlem  26216  usgruspgrb  26275  nbumgrvtx  26441  nbupgrres  26464  isuvtx  26497  isuvtxaOLD  26498  cusgrexilem2  26548  cusgrexi  26549  structtocusgr  26552  cusgrres  26554  cusgrfilem2  26562  vtxdginducedm1  26649  cusconngr  27343  2pthfrgr  27438  frgrncvvdeq  27463  frgrwopreglem4  27469  frgrwopreglem5  27475  frgrwopreg  27477  frgrhash2wsp  27486  strlem1  29418  strlem3  29421  strlem4  29422  strlem5  29423  hstrlem3  29429  hstrlem4  29430  iundisjf  29709  suppss3  29811  iundisjfi  29864  qtophaus  30212  elzdif0  30333  ind0  30389  measvunilem  30584  sibfof  30711  eulerpartlemb  30739  eulerpartlemf  30741  sseqf  30763  ballotlem5  30870  ballotlemi1  30873  ballotlemii  30874  ballotlemic  30877  ballotlem1c  30878  ballotlemscr  30889  ballotlemro  30893  ballotlemfg  30896  ballotlemfrc  30897  ballotlemfrceq  30899  ballotlemrinv0  30903  plymulx0  30933  signstfvn  30955  bnj923  31145  bnj570  31282  bnj594  31289  subfacp1lem1  31468  mrsubcn  31723  mrsubco  31725  circum  31875  dfon2lem6  31998  neibastop1  32660  bj-restn0b  33350  lindsenlbs  33717  matunitlindflem1  33718  poimirlem24  33746  poimirlem25  33747  dvtan  33773  itg2addnclem2  33775  ftc1cnnc  33797  dvasin  33809  dvreasin  33811  dvreacos  33812  isdrngo2  34070  isdrngo3  34071  divrngidl  34140  isfldidl  34180  pridlc2  34184  pridlc3  34185  prter2  34670  lsateln0  34785  lsatlss  34786  lsmsat  34798  lsatcv0  34821  lsat0cv  34823  lcv1  34831  l1cvpat  34844  dih1dimatlem  37120  dihatexv2  37130  djhcvat42  37206  dihjat1lem  37219  dochsatshp  37242  lcfl6  37291  mapdrvallem2  37436  mapdpglem32  37496  irrapx1  37894  pell1234qrne0  37919  pell1234qrreccl  37920  pell1234qrmulcl  37921  pell14qrgt0  37925  pell1234qrdich  37927  pell14qrdich  37935  pell1qrge1  37936  pell1qr1  37937  pell1qrgap  37940  pell14qrgapw  37942  pellqrexplicit  37943  pellqrex  37945  pellfundge  37948  pellfundgt1  37949  setindtr  38093  kelac1  38135  mpaaeu  38222  flcidc  38246  cntzsdrg  38274  deg1mhm  38287  radcnvrat  39015  binomcxplemdvbinom  39054  disjiun2  39725  fiiuncl  39733  disjf1o  39877  difmapsn  39903  supminfxr2  40197  icoiccdif  40253  iccdificc  40269  fsumnncl  40306  fsumsplit1  40307  fsumsupp0  40313  fprod0  40331  climrec  40338  islpcn  40374  lptre2pt  40375  limclner  40386  cnrefiisplem  40558  fprodcncf  40617  fperdvper  40636  dvdivcncf  40645  dvnmul  40661  dvmptfprodlem  40662  dvnprodlem2  40665  stoweidlem25  40745  stoweidlem28  40748  stoweidlem41  40761  stoweidlem44  40764  stoweidlem46  40766  stirlinglem5  40798  dirkercncflem1  40823  dirkercncflem2  40824  fourierdlem24  40851  fourierdlem62  40888  fouriersw  40951  fouriercn  40952  elaa2lem  40953  elaa2  40954  etransclem25  40979  etransclem35  40989  etransclem44  40998  sge0iunmptlemfi  41133  sge0fodjrnlem  41136  iundjiunlem  41179  meadjiunlem  41185  meaiininclem  41206  isomenndlem  41250  hsphoidmvle2  41305  hsphoidmvle  41306  hoidmv1lelem2  41312  hoidmvle  41320  ovnhoilem1  41321  hspdifhsp  41336  hspmbllem2  41347  ovnsubadd2lem  41365  ovolval4lem1  41369  preimagelt  41418  preimalegt  41419  fsummsndifre  41852  fsummmodsndifre  41854  odz2prm2pw  41985  fmtnoprmfac1lem  41986  fmtnoprmfac2lem1  41988  2pwp1prm  42013  lighneallem2  42033  lighneallem3  42034  lighneallem4  42037  bgoldbtbndlem2  42204  bgoldbtbndlem3  42205  bgoldbtbndlem4  42206  bgoldbtbnd  42207  c0rhm  42422  c0rnghm  42423  zrrnghm  42427  2zrngnmlid2  42461  zrinitorngc  42510  zrtermorngc  42511  mgpsumunsn  42650  mgpsumz  42651  mgpsumn  42652  lindslinindsimp1  42756  lindslinindsimp2  42762  lincresunit1  42776  lincresunit2  42777  lincresunit3lem1  42778  lincresunit3lem2  42779  lincresunit3  42780  lindssnlvec  42785  logcxp0  42839  relogbmulbexp  42865  relogbdivb  42866  dignn0fr  42905
  Copyright terms: Public domain W3C validator