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

Theorem eldifi 3716
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 3570 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 476 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1987  cdif 3557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563
This theorem is referenced by:  difss  3721  noel  3901  eqoreldif  4203  eqoreldifOLD  4204  xpdifid  5531  tz7.7  5718  tfi  7015  peano5  7051  wfrlem10  7384  wfrlem15  7389  tz7.48-1  7498  tz7.49  7500  dif20el  7545  oaf1o  7603  oeordi  7627  oeord  7628  oecan  7629  oeword  7630  oeworde  7633  oelimcl  7640  oeeulem  7641  oeeui  7642  oaabs2  7685  boxcutc  7911  domdifsn  8003  isinf  8133  pssnn  8138  pwfilem  8220  fsuppco2  8268  fsuppcor  8269  ordtypelem7  8389  unxpwdom2  8453  inf3lem3  8487  cantnfp1lem1  8535  cantnfp1lem3  8537  infxpenc2lem1  8802  dfacacn  8923  isf32lem3  9137  isf34lem4  9159  fin67  9177  isfin7-2  9178  domtriomlem  9224  axdc2lem  9230  axdc3lem4  9235  axdc4lem  9237  ttukeylem7  9297  konigthlem  9350  fpwwe2lem13  9424  fpwwe2  9425  modfzo0difsn  12698  hashf1lem1  13193  hashle2prv  13214  rlimrege0  14260  rlimrecl  14261  sumrblem  14391  fsumcvg  14392  summolem2a  14395  fsumss  14405  fsumless  14474  cvgcmpce  14496  binomlem  14505  incexclem  14512  incexc  14513  isumltss  14524  prodrblem  14603  fprodcvg  14604  prodmolem2a  14608  fprodss  14622  fprodn0f  14666  fprodeq0g  14669  fprodmodd  14672  rpnnen2lem10  14896  rpnnen2lem11  14897  sumeven  15053  sumodd  15054  lcmfunsnlem2  15296  oddprmge3  15355  oddprm  15458  nnoddn2prm  15459  nnoddn2prmb  15461  iserodd  15483  prmreclem2  15564  prmreclem3  15565  prmreclem5  15567  4sqlem19  15610  prmdvdsprmo  15689  prmodvdslcmf  15694  prmlem0  15755  firest  16033  grpinvnzcl  17427  symgextfv  17778  pmtrf  17815  pmtrdifellem3  17838  sylow2alem2  17973  sylow2a  17974  efgsf  18082  efgsrel  18087  efgs1  18088  efgsfo  18092  efgredlemc  18098  gsumzaddlem  18261  gsumzadd  18262  gsumzmhm  18277  gsum2d2lem  18312  dprdfadd  18359  dprdres  18367  subgdmdprd  18373  dmdprdsplitlem  18376  dmdprdsplit2lem  18384  dpjidcl  18397  ablfac1b  18409  pgpfac1lem1  18413  gsummgp0  18548  isirred  18639  irredrmul  18647  isdrng2  18697  isdrngd  18712  lcomfsupp  18843  lbspropd  19039  lspsneq  19062  lsppratlem6  19092  lbsextlem2  19099  lbsextlem4  19101  ringelnzr  19206  psrbaglesupp  19308  psrlidm  19343  psrridm  19344  mplsubglem  19374  mpllsslem  19375  mplsubrglem  19379  mplmonmul  19404  mplcoe1  19405  mplcoe5  19408  mplbas2  19410  evlslem3  19454  coe1tmmul2  19586  coe1tmmul  19587  xrs1mnd  19724  xrs10  19725  xrs1cmn  19726  cnsubrg  19746  psgnodpm  19874  zrhpsgnodpm  19878  evpmodpmf1o  19882  uvcresum  20072  frlmssuvc1  20073  frlmsslsp  20075  frlmup2  20078  lindfrn  20100  f1lindf  20101  lindfmm  20106  islindf4  20117  dmatmul  20243  1marepvsma1  20329  mdetdiaglem  20344  mdetrlin  20348  mdetrsca  20349  mdetralt  20354  maducoeval2  20386  madugsum  20389  symgmatr01  20400  gsummatr01lem3  20403  gsummatr01lem4  20404  gsummatr01  20405  smadiadetlem0  20407  smadiadetlem1a  20409  cmpfi  21151  2ndcdisj2  21200  elptr2  21317  ptcnplem  21364  xkopt  21398  kqdisj  21475  fin1aufil  21676  ptcmplem2  21797  ptcmplem3  21798  ptcmplem4  21799  opnsubg  21851  lpbl  22248  blcld  22250  zcld  22556  recld2  22557  reconnlem1  22569  divcn  22611  iundisj  23256  mbfeqalem  23349  itg1val2  23391  itg1ge0  23393  i1fmullem  23401  i1fadd  23402  itg1addlem4  23406  itg1mulc  23411  itg1lea  23419  itg1le  23420  mbfi1fseqlem4  23425  itg2uba  23450  itg2lea  23451  itg2eqa  23452  itg2splitlem  23455  itg2split  23456  itgeqa  23520  ellimc3  23583  dvaddbr  23641  dvmulbr  23642  dvcobr  23649  dvcjbr  23652  dvrec  23658  dvcnvlem  23677  dvexp3  23679  dveflem  23680  tdeglem4  23758  deg1n0ima  23787  deg1mul3le  23814  ig1peu  23869  ply1termlem  23897  plypf1  23906  plyaddlem1  23907  plymullem1  23908  coeeulem  23918  coeidlem  23931  coeid3  23934  coefv0  23942  coemulhi  23948  coemulc  23949  dvply1  23977  fta1  24001  vieta1lem2  24004  elaa  24009  elqaalem2  24013  aannenlem2  24022  aaliou2  24033  tayl0  24054  dvtaylp  24062  taylthlem1  24065  taylthlem2  24066  pserdvlem2  24120  logbcl  24439  relogbreexp  24447  relogbcxp  24457  cxplogb  24458  dcubic  24507  rlimcnp  24626  jensen  24649  dmgmaddn0  24683  dmlogdmgm  24684  lgamgulmlem2  24690  igamz  24708  gamp1  24718  regamcl  24721  wilthlem2  24729  basellem3  24743  chpub  24879  logexprlim  24884  lgslem1  24956  lgslem4  24959  lgsvalmod  24975  lgsqr  25010  lgsqrmod  25011  lgsqrmodndvds  25012  gausslemma2dlem0b  25016  gausslemma2dlem0c  25017  gausslemma2dlem0i  25023  gausslemma2dlem1a  25024  gausslemma2dlem4  25028  gausslemma2dlem5a  25029  gausslemma2dlem7  25032  gausslemma2d  25033  lgsquadlem1  25039  lgsquad2  25045  m1lgs  25047  2lgsoddprm  25075  dchrisum0fno1  25134  rplogsum  25150  ishpg  25585  umgrislfupgrlem  25946  usgruspgrb  26003  nbumgrvtx  26163  nbupgrres  26187  isuvtxa  26216  cusgrexilem2  26259  cusgrexi  26260  structtocusgr  26263  cusgrres  26265  cusgrfilem2  26273  cusconngr  26951  2pthfrgr  27046  frgrncvvdeq  27072  frgrhash2wsp  27089  strlem1  28997  strlem3  29000  strlem4  29001  strlem5  29002  hstrlem3  29008  hstrlem4  29009  iundisjf  29288  suppss3  29386  iundisjfi  29438  qtophaus  29727  elzdif0  29848  ind0  29905  measvunilem  30098  sibfof  30225  eulerpartlemb  30253  eulerpartlemf  30255  sseqf  30277  ballotlem5  30384  ballotlemi1  30387  ballotlemii  30388  ballotlemic  30391  ballotlem1c  30392  ballotlemscr  30403  ballotlemro  30407  ballotlemfg  30410  ballotlemfrc  30411  ballotlemfrceq  30413  ballotlemrinv0  30417  plymulx0  30446  signstfvn  30468  bnj923  30599  bnj570  30736  bnj594  30743  subfacp1lem1  30922  mrsubcn  31177  mrsubco  31179  circum  31329  dfon2lem6  31447  neibastop1  32049  bj-restn0b  32734  lindsenlbs  33075  matunitlindflem1  33076  poimirlem24  33104  poimirlem25  33105  dvtan  33131  itg2addnclem2  33133  ftc1cnnc  33155  dvasin  33167  dvreasin  33169  dvreacos  33170  isdrngo2  33428  isdrngo3  33429  divrngidl  33498  isfldidl  33538  pridlc2  33542  pridlc3  33543  prter2  33685  lsateln0  33801  lsatlss  33802  lsmsat  33814  lsatcv0  33837  lsat0cv  33839  lcv1  33847  l1cvpat  33860  dih1dimatlem  36137  dihatexv2  36147  djhcvat42  36223  dihjat1lem  36236  dochsatshp  36259  lcfl6  36308  mapdrvallem2  36453  mapdpglem32  36513  irrapx1  36911  pell1234qrne0  36936  pell1234qrreccl  36937  pell1234qrmulcl  36938  pell14qrgt0  36942  pell1234qrdich  36944  pell14qrdich  36952  pell1qrge1  36953  pell1qr1  36954  pell1qrgap  36957  pell14qrgapw  36959  pellqrexplicit  36960  pellqrex  36962  pellfundge  36965  pellfundgt1  36966  setindtr  37110  kelac1  37152  mpaaeu  37240  flcidc  37264  cntzsdrg  37292  deg1mhm  37305  radcnvrat  38034  binomcxplemdvbinom  38073  disjiun2  38748  fiiuncl  38756  disjf1o  38887  difmapsn  38913  icoiccdif  39196  iccdificc  39212  fsumnncl  39239  fsumsplit1  39240  fsumsupp0  39246  fprod0  39264  climrec  39271  islpcn  39307  lptre2pt  39308  limclner  39319  fprodcncf  39449  dvrecg  39462  fperdvper  39470  dvdivcncf  39479  dvnmul  39495  dvmptfprodlem  39496  dvnprodlem2  39499  stoweidlem25  39579  stoweidlem28  39582  stoweidlem41  39595  stoweidlem44  39598  stoweidlem46  39600  stirlinglem5  39632  dirkercncflem1  39657  dirkercncflem2  39658  fourierdlem24  39685  fourierdlem62  39722  fouriersw  39785  fouriercn  39786  elaa2lem  39787  elaa2  39788  etransclem25  39813  etransclem35  39823  etransclem44  39832  sge0iunmptlemfi  39967  sge0fodjrnlem  39970  iundjiunlem  40013  meadjiunlem  40019  meaiininclem  40037  isomenndlem  40081  hsphoidmvle2  40136  hsphoidmvle  40137  hoidmv1lelem2  40143  hoidmvle  40151  ovnhoilem1  40152  hspdifhsp  40167  hspmbllem2  40178  ovnsubadd2lem  40196  ovolval4lem1  40200  preimagelt  40249  preimalegt  40250  fsummsndifre  40670  fsummmodsndifre  40672  odz2prm2pw  40804  fmtnoprmfac1lem  40805  fmtnoprmfac2lem1  40807  2pwp1prm  40832  lighneallem2  40852  lighneallem3  40853  lighneallem4  40856  bgoldbtbndlem2  41013  bgoldbtbndlem3  41014  bgoldbtbndlem4  41015  bgoldbtbnd  41016  c0rhm  41230  c0rnghm  41231  zrrnghm  41235  2zrngnmlid2  41269  zrinitorngc  41318  zrtermorngc  41319  mgpsumunsn  41458  mgpsumz  41459  mgpsumn  41460  lindslinindsimp1  41564  lindslinindsimp2  41570  lincresunit1  41584  lincresunit2  41585  lincresunit3lem1  41586  lincresunit3lem2  41587  lincresunit3  41588  lindssnlvec  41593  logcxp0  41651  relogbmulbexp  41677  relogbdivb  41678  dignn0fr  41717
  Copyright terms: Public domain W3C validator