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

Theorem eldifi 4100
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 3943 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 498 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2105  cdif 3930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936
This theorem is referenced by:  difss  4105  noelOLD  4294  eqoreldif  4614  xpdifid  6018  tz7.7  6210  tfi  7557  peano5  7594  wfrlem10  7953  wfrlem15  7958  tz7.48-1  8068  tz7.49  8070  dif20el  8119  oaf1o  8178  oeordi  8202  oeord  8203  oecan  8204  oeword  8205  oeworde  8208  oelimcl  8215  oeeulem  8216  oeeui  8217  oaabs2  8261  boxcutc  8493  domdifsn  8588  isinf  8719  pssnn  8724  pwfilem  8806  fsuppco2  8854  fsuppcor  8855  ordtypelem7  8976  unxpwdom2  9040  inf3lem3  9081  cantnfp1lem1  9129  cantnfp1lem3  9131  infxpenc2lem1  9433  dfacacn  9555  isf32lem3  9765  isf34lem4  9787  fin67  9805  isfin7-2  9806  domtriomlem  9852  axdc2lem  9858  axdc3lem4  9863  axdc4lem  9865  ttukeylem7  9925  konigthlem  9978  fpwwe2lem13  10052  fpwwe2  10053  modfzo0difsn  13299  hashf1lem1  13801  hashle2prv  13824  rlimrege0  14924  rlimrecl  14925  sumrblem  15056  fsumcvg  15057  summolem2a  15060  fsumss  15070  fsumless  15139  cvgcmpce  15161  binomlem  15172  incexclem  15179  incexc  15180  isumltss  15191  prodrblem  15271  fprodcvg  15272  prodmolem2a  15276  fprodss  15290  fprodn0f  15333  fprodeq0g  15336  fprodmodd  15339  rpnnen2lem10  15564  rpnnen2lem11  15565  sumeven  15726  sumodd  15727  lcmfunsnlem2  15972  oddprmge3  16032  oddprm  16135  nnoddn2prm  16136  nnoddn2prmb  16138  iserodd  16160  prmreclem2  16241  prmreclem3  16242  prmreclem5  16244  4sqlem19  16287  prmdvdsprmo  16366  prmodvdslcmf  16371  prmlem0  16427  firest  16694  grpinvnzcl  18109  symgextfv  18475  pmtrf  18512  pmtrdifellem3  18535  sylow2alem2  18672  sylow2a  18673  efgsf  18784  efgsrel  18789  efgs1  18790  efgsfo  18794  gsumzaddlem  18970  gsumzadd  18971  gsumzmhm  18986  gsum2d2lem  19022  dprdfadd  19071  dprdres  19079  subgdmdprd  19085  dmdprdsplitlem  19088  dmdprdsplit2lem  19096  dpjidcl  19109  ablfac1b  19121  pgpfac1lem1  19125  gsummgp0  19287  isirred  19378  irredrmul  19386  isdrng2  19441  isdrngd  19456  cntzsdrg  19510  lcomfsupp  19603  lbspropd  19800  lspsneq  19823  lsppratlem6  19853  lbsextlem2  19860  lbsextlem4  19862  ringelnzr  19967  psrbaglesupp  20076  psrlidm  20111  psrridm  20112  mplsubglem  20142  mpllsslem  20143  mplsubrglem  20147  mplmonmul  20173  mplcoe1  20174  mplcoe5  20177  mplbas2  20179  evlslem3  20221  mhpvscacl  20269  coe1tmmul2  20372  coe1tmmul  20373  xrs1mnd  20511  xrs10  20512  xrs1cmn  20513  cnsubrg  20533  psgnodpm  20660  zrhpsgnodpm  20664  evpmodpmf1o  20668  uvcresum  20865  frlmssuvc1  20866  frlmsslsp  20868  frlmup2  20871  lindfrn  20893  f1lindf  20894  lindfmm  20899  islindf4  20910  dmatmul  21034  1marepvsma1  21120  mdetdiaglem  21135  mdetrlin  21139  mdetrsca  21140  mdetralt  21145  maducoeval2  21177  madugsum  21180  symgmatr01  21191  gsummatr01lem3  21194  gsummatr01lem4  21195  gsummatr01  21196  smadiadetlem0  21198  smadiadetlem1a  21200  cmpfi  21944  2ndcdisj2  21993  elptr2  22110  ptcnplem  22157  xkopt  22191  kqdisj  22268  fin1aufil  22468  ptcmplem2  22589  ptcmplem3  22590  ptcmplem4  22591  opnsubg  22643  lpbl  23040  blcld  23042  zcld  23348  recld2  23349  reconnlem1  23361  divcn  23403  iundisj  24076  mbfeqalem1  24169  itg1val2  24212  itg1ge0  24214  i1fmullem  24222  i1fadd  24223  itg1addlem4  24227  itg1mulc  24232  itg1lea  24240  itg1le  24241  mbfi1fseqlem4  24246  itg2uba  24271  itg2lea  24272  itg2eqa  24273  itg2splitlem  24276  itg2split  24277  itgeqa  24341  ellimc3  24404  dvaddbr  24462  dvmulbr  24463  dvcobr  24470  dvcjbr  24473  dvrec  24479  dvrecg  24497  dvcnvlem  24500  dvexp3  24502  dveflem  24503  tdeglem4  24581  deg1n0ima  24610  deg1mul3le  24637  ig1peu  24692  ply1termlem  24720  plypf1  24729  plyaddlem1  24730  plymullem1  24731  coeeulem  24741  coeidlem  24754  coeid3  24757  coefv0  24765  coemulhi  24771  coemulc  24772  dvply1  24800  fta1  24824  vieta1lem2  24827  elaa  24832  elqaalem2  24836  aannenlem2  24845  aaliou2  24856  tayl0  24877  dvtaylp  24885  taylthlem1  24888  taylthlem2  24889  pserdvlem2  24943  logbcl  25272  relogbreexp  25280  relogbcxp  25290  cxplogb  25291  dcubic  25351  rlimcnp  25470  jensen  25493  dmgmaddn0  25527  dmlogdmgm  25528  lgamgulmlem2  25534  igamz  25552  gamp1  25562  regamcl  25565  wilthlem2  25573  basellem3  25587  chpub  25723  logexprlim  25728  lgslem1  25800  lgslem4  25803  lgsvalmod  25819  lgsqr  25854  lgsqrmod  25855  lgsqrmodndvds  25856  gausslemma2dlem0b  25860  gausslemma2dlem0c  25861  gausslemma2dlem0i  25867  gausslemma2dlem1a  25868  gausslemma2dlem4  25872  gausslemma2dlem5a  25873  gausslemma2dlem7  25876  gausslemma2d  25877  lgsquad2  25889  m1lgs  25891  2lgsoddprm  25919  2sqreultblem  25951  dchrisum0fno1  26014  rplogsum  26030  ishpg  26472  elntg2  26698  umgrislfupgrlem  26834  usgruspgrb  26893  nbumgrvtx  27055  nbupgrres  27073  isuvtx  27104  cusgrexilem2  27151  cusgrexi  27152  structtocusgr  27155  cusgrres  27157  cusgrfilem2  27165  vtxdginducedm1  27252  cusconngr  27897  2pthfrgr  27990  frgrncvvdeq  28015  frgrwopreglem4  28021  frgrwopreglem5  28027  frgrwopreg  28029  frgrhash2wsp  28038  strlem1  29954  strlem3  29957  strlem4  29958  strlem5  29959  hstrlem3  29965  hstrlem4  29966  iundisjf  30267  suppss3  30386  iundisjfi  30445  qtophaus  30999  elzdif0  31120  ind0  31176  measvunilem  31370  sibfof  31497  eulerpartlemb  31525  eulerpartlemf  31527  sseqf  31549  ballotlem5  31656  ballotlemi1  31659  ballotlemii  31660  ballotlemic  31663  ballotlem1c  31664  ballotlemscr  31675  ballotlemro  31679  ballotlemfg  31682  ballotlemfrc  31683  ballotlemfrceq  31685  ballotlemrinv0  31689  plymulx0  31716  signstfvn  31738  signsvfn  31751  bnj923  31938  bnj570  32076  bnj594  32083  subfacp1lem1  32323  satffunlem2lem1  32548  mrsubcn  32663  mrsubco  32665  circum  32814  dfon2lem6  32930  frrlem12  33031  frrlem13  33032  neibastop1  33604  bj-restn0b  34276  lindsadd  34766  lindsenlbs  34768  matunitlindflem1  34769  poimirlem24  34797  poimirlem25  34798  dvtan  34823  itg2addnclem2  34825  ftc1cnnc  34847  dvasin  34859  dvreasin  34861  dvreacos  34862  isdrngo2  35117  isdrngo3  35118  divrngidl  35187  isfldidl  35227  pridlc2  35231  pridlc3  35232  prter2  35897  lsateln0  36011  lsatlss  36012  lsmsat  36024  lsatcv0  36047  lsat0cv  36049  lcv1  36057  l1cvpat  36070  dih1dimatlem  38345  dihatexv2  38355  djhcvat42  38431  dihjat1lem  38444  dochsatshp  38467  lcfl6  38516  mapdrvallem2  38661  mapdpglem32  38721  prjspertr  39133  prjsperref  39134  prjspersym  39135  prjspvs  39138  prjsprellsp  39139  dffltz  39149  irrapx1  39303  pell1234qrne0  39328  pell1234qrreccl  39329  pell1234qrmulcl  39330  pell14qrgt0  39334  pell1234qrdich  39336  pell14qrdich  39344  pell1qrge1  39345  pell1qr1  39346  pell1qrgap  39349  pell14qrgapw  39351  pellqrexplicit  39352  pellqrex  39354  pellfundge  39357  pellfundgt1  39358  setindtr  39499  kelac1  39541  mpaaeu  39628  flcidc  39652  deg1mhm  39685  radcnvrat  40523  binomcxplemdvbinom  40562  disjiun2  41197  fiiuncl  41204  disjf1o  41328  difmapsn  41351  supminfxr2  41621  icoiccdif  41676  iccdificc  41691  fsumnncl  41728  fsumsplit1  41729  fsumsupp0  41735  fprod0  41753  climrec  41760  islpcn  41796  lptre2pt  41797  limclner  41808  cnrefiisplem  41986  fprodcncf  42060  fperdvper  42079  dvdivcncf  42088  dvnmul  42104  dvmptfprodlem  42105  dvnprodlem2  42108  stoweidlem25  42187  stoweidlem28  42190  stoweidlem41  42203  stoweidlem44  42206  stoweidlem46  42208  stirlinglem5  42240  dirkercncflem1  42265  dirkercncflem2  42266  fourierdlem24  42293  fourierdlem62  42330  fouriersw  42393  fouriercn  42394  elaa2lem  42395  elaa2  42396  etransclem25  42421  etransclem35  42431  etransclem44  42440  sge0iunmptlemfi  42572  sge0fodjrnlem  42575  iundjiunlem  42618  meadjiunlem  42624  meaiininclem  42645  isomenndlem  42689  hsphoidmvle2  42744  hsphoidmvle  42745  hoidmv1lelem2  42751  hoidmvle  42759  ovnhoilem1  42760  hspdifhsp  42775  hspmbllem2  42786  ovnsubadd2lem  42804  ovolval4lem1  42808  preimagelt  42857  preimalegt  42858  fsummsndifre  43409  fsummmodsndifre  43411  odz2prm2pw  43602  fmtnoprmfac1lem  43603  fmtnoprmfac2lem1  43605  2pwp1prm  43628  lighneallem2  43648  lighneallem3  43649  lighneallem4  43652  bgoldbtbndlem2  43848  bgoldbtbndlem3  43849  bgoldbtbndlem4  43850  bgoldbtbnd  43851  c0rhm  44111  c0rnghm  44112  zrrnghm  44116  2zrngnmlid2  44150  zrinitorngc  44199  zrtermorngc  44200  mgpsumunsn  44337  mgpsumz  44338  mgpsumn  44339  lindslinindsimp1  44440  lindslinindsimp2  44446  lincresunit1  44460  lincresunit2  44461  lincresunit3lem1  44462  lincresunit3lem2  44463  lincresunit3  44464  lindssnlvec  44469  logcxp0  44523  relogbmulbexp  44549  relogbdivb  44550  dignn0fr  44589  rrxlinesc  44650  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653
  Copyright terms: Public domain W3C validator