MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq2d Structured version   Unicode version

Theorem eleq2d 2521
Description: Deduction from equality to equivalence of membership. Revised to reduce dependencies on axioms. (Contributed by NM, 27-Dec-1993.) (Revised by Wolf Lammen, 5-Dec-2019.)
Hypothesis
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eleq2d  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2d
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq1d.1 . . . 4  |-  ( ph  ->  A  =  B )
2 dfcleq 2444 . . . 4  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
31, 2sylib 196 . . 3  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
4 bi1 186 . . . . . 6  |-  ( ( x  e.  A  <->  x  e.  B )  ->  (
x  e.  A  ->  x  e.  B )
)
54anim2d 565 . . . . 5  |-  ( ( x  e.  A  <->  x  e.  B )  ->  (
( x  =  C  /\  x  e.  A
)  ->  ( x  =  C  /\  x  e.  B ) ) )
65aleximi 1623 . . . 4  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  ->  ( E. x ( x  =  C  /\  x  e.  A )  ->  E. x
( x  =  C  /\  x  e.  B
) ) )
7 bi2 198 . . . . . 6  |-  ( ( x  e.  A  <->  x  e.  B )  ->  (
x  e.  B  ->  x  e.  A )
)
87anim2d 565 . . . . 5  |-  ( ( x  e.  A  <->  x  e.  B )  ->  (
( x  =  C  /\  x  e.  B
)  ->  ( x  =  C  /\  x  e.  A ) ) )
98aleximi 1623 . . . 4  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  ->  ( E. x ( x  =  C  /\  x  e.  B )  ->  E. x
( x  =  C  /\  x  e.  A
) ) )
106, 9impbid 191 . . 3  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
113, 10syl 16 . 2  |-  ( ph  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x ( x  =  C  /\  x  e.  B ) ) )
12 df-clel 2446 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
13 df-clel 2446 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
1411, 12, 133bitr4g 288 1  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1368    = wceq 1370   E.wex 1587    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2443  df-clel 2446
This theorem is referenced by:  eleq2  2524  eleq12d  2533  eleqtrd  2541  neleqtrd  2563  neleqtrrdOLD  2565  abeq2d  2577  nfceqdf  2608  drnfc1  2631  drnfc2  2632  sbcbid  3342  cbvcsb  3391  csbie2g  3416  cbvralcsf  3417  cbvreucsf  3419  cbvrabcsf  3420  sbcel12  3773  sbcel1g  3779  sbcel2  3781  csbeq2d  3784  prel12g  4150  iuneq12df  4292  cbviun  4305  cbviin  4306  iinxsng  4345  iinxprg  4346  iunxsng  4347  cbvdisj  4370  disjor  4374  mpteq12f  4466  axpweq  4567  rabxfrd  4611  0nelelxp  4966  opeliunxp  4988  opeliunxp2  5076  iunxpf  5086  elrelimasn  5291  elimasng  5293  elimasni  5294  xpdifid  5364  ressn  5471  funfni  5609  fnbr  5611  dffv3  5785  fvelrnb  5838  fvun1  5861  fvco2  5865  elpreima  5922  dff3  5955  fmptco  5975  fnelfp  6005  fnelnfp  6007  fnprb  6035  fnprOLD  6036  funfvima3  6053  eluniima  6066  dff13  6070  f1eqcocnv  6098  isoini  6128  riotaeqdv  6152  mpt2eq123dva  6246  cbvmpt2x  6263  ovelrn  6339  elovmpt2  6407  fun11iun  6637  zfrep6  6645  fmpt2x  6740  bropopvvv  6753  elsuppfn  6798  suppfnss  6814  mpt2xopn0yelv  6830  mpt2xopovel  6837  isprmpt2  6843  rntpos  6858  mpt2curryd  6888  onoviun  6904  smoel  6921  smoiso  6923  smoel2  6924  smo11  6925  tfrlem9  6944  oalimcl  7099  oaass  7100  omordi  7105  omordlim  7116  omlimcl  7117  odi  7118  omeulem1  7121  omeulem2  7122  oen0  7125  oeordi  7126  oeordsuc  7133  oelimcl  7139  oeeulem  7140  oeeui  7141  nnmordi  7170  oaabs2  7184  omabs  7186  omsmolem  7192  ereldm  7244  iiner  7272  elmapg  7327  elpmg  7328  elixpsn  7402  ixpsnf1o  7403  boxriin  7405  omxpenlem  7512  pw2f1olem  7515  phplem4  7593  php3  7597  elfi  7764  dffi3  7782  marypha2lem2  7787  ordiso2  7830  wemapsolem  7865  elharval  7879  inf3lemd  7934  inf3lem1  7935  inf3lem2  7936  inf3lem3  7937  cantnfs  7975  cantnfp1lem3  7989  cantnflem1b  7995  cantnflem1  7998  cantnfsOLD  8005  cantnfp1lem3OLD  8015  cantnflem1bOLD  8018  cantnflem1OLD  8021  trcl  8049  r1sdom  8082  r1ordg  8086  r1pwss  8092  tz9.12lem3  8097  tz9.12  8098  r1elwf  8104  rankr1ai  8106  rankidb  8108  rankr1bg  8111  rankval2  8126  rankunb  8158  tcrank  8192  fseqdom  8297  acni  8316  acni2  8317  acndom  8322  infpwfien  8333  alephnbtwn  8342  cardaleph  8360  cardinfima  8368  iunfictbso  8385  dfac3  8392  dfac5lem5  8398  dfac5  8399  dfac9  8406  dfac12r  8416  kmlem2  8421  kmlem12  8431  kmlem13  8432  kmlem14  8433  ackbij2lem3  8511  ackbij2  8513  cofsmo  8539  cfsmolem  8540  alephsing  8546  fin23lem30  8612  isf32lem9  8631  itunisuc  8689  axcc2lem  8706  axcc3  8708  domtriomlem  8712  axdc2lem  8718  axdc2  8719  axdc3lem2  8721  axdc3lem4  8723  axdc4lem  8725  ac6c4  8751  zorn2lem1  8766  ttukeylem6  8784  pwcfsdom  8848  axregndlem2  8870  axinfndlem1  8873  axacndlem4  8878  axacnd  8880  pwfseqlem1  8926  inar1  9043  inatsk  9046  gruurn  9066  grur1  9088  grothpw  9094  eltskm  9111  genpelv  9270  eluz1  10966  eluzadd  10990  eluzsub  10991  elixx1  11410  elixx3g  11414  elioo2  11442  elfz1  11543  elfz2  11545  elfzp1  11606  fzpr  11612  fzsuc2  11615  fzrev3  11623  elfzp12  11640  elfzo  11656  elfzom1b  11727  fzosplitsni  11735  zmodidfzo  11838  seqp1  11922  seqf1o  11948  bcval  12181  bcpasc  12198  hash2prd  12283  hashf1lem1  12310  ccatfval  12375  elfzelfzccat  12381  ccatlid  12386  ccatass  12388  swrdid  12423  swrd0len0  12431  swrd0fv  12437  swrdeq  12442  swrdspsleq  12444  ccatswrd  12452  swrdccat2  12454  swrdswrd  12456  swrdswrd0  12458  cats1un  12472  swrdccatfn  12475  swrdccatin1  12476  swrdccatin12lem1  12477  swrdccatin12lem2b  12479  swrdccatin2  12480  swrdccatin12lem2c  12481  swrdccatin12lem2  12482  swrdccat3blem  12488  swrdccatin1d  12492  swrdccatin2d  12493  swrdccatin12d  12494  revccat  12508  revrev  12509  repswccat  12525  cshwidxmod  12542  2cshw  12549  revco  12564  ccatco  12565  cshco  12566  swrdco  12567  shftfn  12664  shftval  12665  limsupgle  13057  ello12  13096  elo12  13107  isercolllem3  13246  sumeq1  13268  fsumsplit  13318  sumsplit  13337  fsum2dlem  13339  fsumcom2  13343  fsumparts  13371  explecnv  13429  eftlub  13495  divalgmod  13712  bitsval  13722  bitsp1e  13730  bitsp1o  13731  sadfval  13750  sadcp1  13753  sadval  13754  sadcadd  13756  sadadd2  13758  saddisjlem  13762  sadadd  13765  sadass  13769  smufval  13775  smuval  13779  smuval2  13780  smupvallem  13781  smu01lem  13783  smueqlem  13788  smumul  13791  bezoutlem2  13825  bezoutlem4  13827  algfx  13857  eucalgcvga  13863  reumodprminv  13974  nnnn0modprm0  13976  unbenlem  14071  prmreclem5  14083  vdwapval  14136  vdwapun  14137  vdwnnlem1  14158  vdwnn  14161  ramval  14171  0ram  14183  ramub1lem2  14190  prmlem0  14235  elrest  14468  prdsbasmpt  14510  prdsleval  14517  prdsbasmpt2  14522  pwselbasb  14528  imasaddfnlem  14568  imasvscafn  14577  divsfval  14587  ismre  14630  mreunirn  14641  mrisval  14670  ismri  14671  isacs  14691  catidd  14720  iscatd2  14721  ismon  14774  isepi  14781  sectffval  14791  sectfval  14792  issubc  14850  isfunc  14876  funcres  14908  funcpropd  14912  ffthiso  14941  isnat  14959  isnat2  14960  fuciso  14987  arwhoma  15015  elsetchom  15051  setcmon  15057  setcepi  15058  setciso  15061  catciso  15077  hofcl  15171  hofpropd  15179  yonedalem4c  15189  yonedainv  15193  yonffthlem  15194  lubeldm  15253  glbeldm  15266  joindef  15276  meetdef  15290  poslubdg  15421  acsficl2d  15448  acsmapd  15450  psref  15480  psss  15486  dirge  15509  grpidval  15534  grpidd  15545  ismndd  15546  mndpropd  15548  grpidpropd  15549  imasmnd2  15560  imasmnd  15561  ismhm  15568  issubm  15577  gsumccat  15621  imasgrp2  15772  imasgrp  15773  issubg  15783  subginv  15790  isnsg  15812  isghm  15849  resghm2b  15867  conjnmzb  15883  conjnsg  15884  ghmpropd  15886  isga  15911  elcntz  15942  elcntzsn  15945  cntzrcl  15947  resscntz  15951  symgextf1  16028  gsmsymgreqlem2  16038  f1otrspeq  16055  pmtrfrn  16066  pmtrdifellem3  16086  pmtrdifellem4  16087  psgnunilem1  16101  psgnunilem5  16102  psgnunilem2  16103  psgnunilem3  16104  psgneldm2  16112  psgnfitr  16125  psgnsn  16128  gexdvds  16187  gex1  16194  isslw  16211  sylow3lem2  16231  lsmelvalx  16243  pj1ghm  16304  efgtlen  16327  efgs1b  16337  efgsfo  16340  efgredlemc  16346  frgp0  16361  frgpmhm  16366  divsabl  16451  frgpnabllem1  16455  0cyg  16473  cycsubgcyg  16481  gsumval3OLD  16486  gsumval3  16489  gsumcllem  16490  gsumcllemOLD  16491  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumzsplit  16522  gsumzsplitOLD  16523  gsummptfzcl  16565  eldprd  16591  eldprdOLD  16593  dprdcntz2  16641  dprd2d2  16648  dmdprdsplit2lem  16649  dmdprdsplit2  16650  dprdsplit  16652  ablfac2  16695  isrngd  16785  imasrng  16817  dvdsrval  16843  isunit  16855  dvdsrpropd  16894  isirred  16897  isrhm  16917  isrim0  16919  drngunit  16943  isdrngd  16963  issubrg  16971  opprsubrg  16992  rhmpropd  17006  isabv  17010  issrngd  17052  islmod  17058  lmodprop2d  17113  islss  17122  islssd  17123  lssats2  17187  lspsnel  17190  islmhm  17214  lmhmf1o  17233  lmhmima  17234  lmhmpreima  17235  reslmhm  17239  pwssplit3  17248  lmhmpropd  17260  islbs  17263  lspprel  17281  lspfixed  17315  lbsacsbs  17343  lbsextlem1  17345  lbsextlem2  17346  lbsextlem3  17347  lbsextlem4  17348  ixpsnbasval  17396  lidlmcl  17405  divscrng  17428  islpidl  17434  lidldvgen  17443  mplsubglem  17617  mpllsslem  17618  mplsubglemOLD  17619  mpllsslemOLD  17620  mplmonmul  17650  mplrcl  17678  subrgascl  17687  subrgasclcl  17688  mpfind  17729  gsumply1subr  17795  strov2rcl  17799  zrhrhmb  18051  znf1o  18093  frgpcyg  18115  psgnevpmb  18126  isphld  18192  elocv  18202  iscss  18217  isobs  18254  obs2ss  18263  dsmmbas2  18271  dsmmfi  18272  dsmmelbas  18273  dsmmlss  18278  frlmelbas  18291  frlmelbasOLD  18292  frlmlbs  18334  frlmup1  18335  ellspd  18339  ellspdOLD  18340  islinds  18347  islindf2  18352  f1lindf  18360  islindf4  18376  matbas2d  18433  matecl  18435  matvscl  18442  mat1  18445  mdetunilem7  18540  mdetunilem9  18542  smadiadetr  18597  cramerimplem2  18606  cramer0  18612  istopon  18646  eltg  18678  eltg2  18679  eltop  18695  eltop2  18696  eltop3  18697  pptbas  18728  iscld  18747  neiss2  18821  isnei  18823  neiptopnei  18852  neiptopreu  18853  lpfval  18858  lpval  18859  islp  18860  maxlp  18867  islpi  18869  neitr  18900  restlp  18903  ordtbas2  18911  ordtrest2  18924  lmfval  18952  cnfval  18953  iscn  18955  iscnp  18957  tgcn  18972  tgcnp  18973  lmbrf  18980  cnpresti  19008  ist1  19041  ist1-2  19067  cnt1  19070  haust1  19072  cmpfi  19127  cmpfii  19128  1stcfb  19165  2ndc1stc  19171  1stcrest  19173  2ndcdisj  19176  1stcelcls  19181  nllyi  19195  subislly  19201  kgenval  19224  elkgen  19225  kgencn2  19246  txbas  19256  eltx  19257  ptval  19259  ptpjpre1  19260  ptopn2  19273  ptpjopn  19301  ptclsg  19304  xkoccn  19308  txdis  19321  txdis1cn  19324  ptrescn  19328  hausdiag  19334  hauseqlcld  19335  txhaus  19336  xkohaus  19342  elqtop  19386  qtopeu  19405  kqcldsat  19422  hmeofval  19447  ptuncnv  19496  ptunhmeo  19497  elmptrab  19516  fbdmn0  19523  elfg  19560  elfilss  19565  filunirn  19571  fixufil  19611  elfm  19636  rnelfmlem  19641  rnelfm  19642  fmfnfmlem4  19646  elflim2  19653  flimtopon  19659  elflim  19660  hausflim  19670  flimcls  19674  flfnei  19680  isflf  19682  hausflf  19686  cnpflf  19690  cnflf  19691  txflf  19695  isfcls  19698  fclstopon  19701  isfcls2  19702  fclssscls  19707  fclsnei  19708  fclsfnflim  19716  flimfnfcls  19717  isfcf  19723  fcfelbas  19725  cnpfcf  19730  cnfcf  19731  alexsublem  19732  alexsubALTlem3  19737  cnextfun  19752  cnextfvval  19753  cnextf  19754  cnextcn  19755  tmdgsum2  19783  tgpconcomp  19799  ghmcnp  19801  divstgplem  19807  eltsms  19819  haustsms  19822  tsmsgsum  19825  tsmsgsumOLD  19828  tsmssubm  19832  tsmssplit  19842  isust  19894  elrnust  19915  ustbas  19918  elutop  19924  ustuqtoplem  19930  ustuqtop4  19935  ustuqtop  19937  utopsnneiplem  19938  utopsnneip  19939  utopsnnei  19940  isusp  19952  isucn  19969  ucncn  19976  iscfilu  19979  neipcfilu  19987  iscusp  19990  cnextucn  19994  ispsmet  19996  ismet  20014  isxmet  20015  elblps  20078  elbl  20079  elmopn  20133  prdsbl  20182  neibl  20192  met1stc  20212  metrest  20215  prdsxmslem2  20220  txmetcnp  20238  txmetcn  20239  metuvalOLD  20240  metuval  20241  metustsymOLD  20252  metustsym  20253  cfilucfil2OLD  20264  cfilucfil2  20265  elbl4  20267  metuelOLD  20268  metuel  20269  metutopOLD  20273  psmetutop  20274  restmetu  20278  metucnOLD  20279  metucn  20280  tngngp  20356  isnmhm  20441  zcld  20506  metnrmlem1a  20550  elcncf  20581  cncfcnvcn  20613  cnheibor  20643  lebnumlem1  20649  ishtpy  20660  isphtpy  20669  om1elbas  20720  elpi1  20733  pi1xfr  20743  pi1coghm  20749  tchcph  20868  lmmbrf  20889  iscfil  20892  iscau  20903  iscauf  20907  caucfil  20910  iscmet  20911  cmetcaulem  20915  iscmet3lem1  20918  iscmet3lem2  20919  iscmet3  20920  bcthlem1  20951  cmsss  20977  cmetcusp1OLD  20979  cmetcusp1  20980  cmetcuspOLD  20981  cmetcusp  20982  rrxcph  21012  minveclem3b  21031  ovolfioo  21067  ovolficc  21068  ovolctb  21089  ovoliunnul  21106  ovolshftlem1  21108  sca2rab  21111  ovolscalem1  21112  ovolicc2lem1  21116  ovolicc2lem2  21117  ovolicc2lem4  21119  ovolicc2lem5  21120  iundisj  21145  iunmbl2  21154  uniioombllem3  21181  vitalilem2  21205  vitalilem3  21206  mbfss  21240  i1faddlem  21287  i1fmullem  21288  mbfi1fseqlem2  21310  mbfi1fseqlem4  21312  mbfi1fseq  21315  itg2splitlem  21342  itg2split  21343  itg2monolem1  21344  itg2gt0  21354  isibl  21359  iblss2  21399  itgss3  21408  itgsplit  21429  ellimc  21464  limcmo  21473  cnlimc  21479  limciun  21485  limcun  21486  eldv  21489  dvbsss  21493  dvreslem  21500  elcpn  21524  dvaddf  21532  dvmulf  21533  dvcof  21538  rolle  21578  dvlip2  21583  dvivthlem1  21596  lhop1  21602  lhop2  21603  ftc1cn  21631  fta1glem2  21754  plyco0  21776  elply  21779  ply1termlem  21787  eltayl  21941  tayl0  21943  taylplem1  21944  taylplem2  21945  dvtaylp  21951  taylthlem1  21954  taylthlem2  21955  abelth  22022  cxpcn3  22302  rlimcnp  22475  fsumharmonic  22521  dchrelbas  22691  pntrsumbnd2  22932  ostth2lem2  22999  istrkgb  23032  istrkgcb  23033  istrkge  23034  istrkgl  23035  istrkg2d  23036  istrkgld  23037  axtgsegcon  23041  axtg5seg  23042  axtgbtwnid  23043  axtgpasch  23044  axtgupdim2  23049  axtgeucl  23050  tgdim01  23078  iscgrg  23084  tglnunirn  23101  tglngne  23103  tglngval  23104  tgellng  23106  legval  23136  legov  23137  legov2  23138  mirreu3  23184  mirval  23185  mirfv  23186  mircgr  23187  mirbtwn  23188  ismir  23189  mireq  23195  symquadlem  23209  israg  23217  perpln1  23229  perpln2  23230  isperp  23231  f1otrgitv  23251  f1otrg  23252  f1otrge  23253  ttgval  23256  ttgelitv  23264  elee  23275  brbtwn  23280  brcgr  23281  axlowdimlem16  23338  ebtwntg  23363  usgra2edg1  23437  usgraidx2vlem1  23444  usgraidx2vlem2  23445  nbgraop  23470  nbgrael  23472  nbgraeledg  23476  nbgraf1olem1  23485  nbgraf1olem3  23487  nbgraf1olem5  23489  nbgraf1o  23491  iscusgra  23499  sizeusglecusglem1  23527  isuvtx  23531  uvtxel  23532  uvtxisvtx  23533  wlks  23560  iswlk  23561  istrl  23571  ispth  23602  isspth  23603  fargshiftlem  23655  fargshiftfv  23656  fargshiftfo  23659  vdgrfval  23700  vdgrun  23706  vdgrfiun  23707  vdgr1a  23711  eupap1  23732  eupath2lem3  23735  ex-res  23783  isabloda  23921  issubgo  23925  isass  23938  elghomlem2  23984  ghablo  23991  iscom2  24034  rngoidmlem  24045  rngo1cl  24051  isssp  24257  sspn  24269  islno  24288  isblo  24317  nmlno0  24330  ishmo  24346  dipdir  24377  dipass  24380  ubthlem1  24406  ubthlem2  24407  htthlem  24454  htth  24455  ocel  24819  ocnel  24836  shsel  24852  shsel2  24860  shmodsi  24927  pjhtheu  24932  pjeq  24937  axpjpj  24958  pjoc2  24977  elspani  25081  h1de2ctlem  25093  elspansn  25104  elspansn2  25105  elnlfn  25467  eleigvec  25496  riesz3i  25601  iuneq12daf  26042  iunrdx  26048  cbvdisjf  26051  disjorf  26057  disjabrex  26060  disjabrexf  26061  iundisjf  26065  disjrdx  26067  elunirn2  26100  abfmpunirn  26101  abfmpeld  26103  abfmpel  26104  fmptcof2  26113  funcnvmptOLD  26120  funcnvmpt  26121  suppss3  26161  fpwrelmap  26167  xrofsup  26189  iundisjfi  26214  eliccioo  26240  inftmrel  26331  isinftm  26332  isslmd  26352  gsummpt2co  26383  xrge0tsmsbi  26388  rngurd  26390  resv1r  26439  metidval  26451  pstmval  26456  cnre2csqima  26475  ordtrest2NEW  26487  fmcncfil  26495  fsumcvg4  26514  ofcfval  26674  measvuni  26762  meascnbl  26767  faeval  26796  ismbfm  26801  elunirnmbfm  26802  isanmbfm  26805  imambfm  26811  itgeq12dv  26846  issibf  26853  eulerpartlems  26877  eulerpartlemgc  26879  eulerpartlemgvv  26893  eulerpartlemgu  26894  eulerpart  26899  rrvmbfm  26959  elorvc  26976  elorrvc  26980  dstfrvunirn  26991  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemsima  27032  ballotlemrv  27036  fzssfzo  27068  ofccat  27075  signstfvn  27104  signstfvneq0  27107  signstres  27110  afsval  27129  brafs  27130  subfacp1lem2b  27203  subfacp1lem4  27205  subfacp1lem5  27206  subfacp1lem6  27207  ptpcon  27256  cvmscbv  27281  iscvm  27282  cvmsi  27288  cvmsval  27289  cvmliftmolem1  27304  cvmlift2lem12  27337  cvmlift2lem13  27338  cvmlift3lem7  27348  snmlval  27354  elgiso  27449  fprodser  27596  fprodsplit  27610  fprod2dlem  27625  fprodcom2  27629  mpteq12d  27717  opelco3  27723  predbrg  27781  trpredrec  27836  wfrlem9  27866  wfrlem12  27869  wsuclem  27896  fvnobday  27957  nodenselem3  27958  nodenselem5  27960  nofulllem5  27981  funtransport  28196  fvtransport  28197  brcolinear  28224  colineardim1  28226  funray  28305  fvray  28306  funline  28307  fvline  28309  lineelsb2  28313  rankelg  28340  rankeq1o  28343  elhf2  28347  0hf  28349  fin2so  28554  ptrest  28563  heicant  28564  mblfinlem1  28566  mblfinlem2  28567  volsupnfl  28574  dvtanlem  28579  itg2addnclem  28581  itg2gt0cn  28585  islocfin  28706  lfinpfin  28713  locfindis  28715  locfincf  28716  comppfsc  28717  neibastop2lem  28719  neibastop3  28721  eltail  28733  indexdom  28766  incsequz  28782  istotbnd  28806  istotbnd3  28808  0totbnd  28810  sstotbnd  28812  sstotbnd3  28813  isbnd  28817  prdstotbnd  28831  cntotbnd  28833  isismty  28838  heibor1lem  28846  heiborlem2  28849  heiborlem3  28850  heibor  28858  exidcl  28879  exidreslem  28880  divrngcl  28901  isdrngo2  28902  isrngohom  28909  isrngoiso  28922  isriscg  28928  iscringd  28937  isidl  28952  ispridl  28972  ismaxidl  28978  ac6s6  29122  prter3  29165  isnacs  29178  mrefg2  29181  elmzpcl  29200  mzpcompact2  29227  eldiophb  29233  elpell1qr  29326  elpell14qr  29328  elpell1234qr  29330  pw2f1ocnv  29524  pw2f1o2val2  29527  aomclem4  29548  aomclem6  29550  islssfg2  29562  imasgim  29593  lnr2i  29610  elmnc  29631  rngunsnply  29668  issdrg  29692  dvconstbi  29746  stoweidlem27  29960  stoweidlem29  29962  stoweidlem31  29964  stoweidlem34  29967  stoweidlem48  29981  stoweidlem59  29992  afvelrnb  30207  afvelrnb0  30208  elfvmptrab1  30292  elfvmptrab  30293  elovmpt2rab  30296  elovmpt2rab1  30297  elovmpt3rab1  30301  elovmpt2wrd  30394  ccatw2s1p1  30407  wlkelwrd  30418  wlkcompim  30425  usg2wlkeq  30427  usgra2pthlem1  30438  wwlk  30453  iswwlk  30455  iswwlkn  30456  wlkiswwlk1  30462  wwlknred  30493  wwlknext  30494  wwlknredwwlkn  30496  wwlknredwwlkn0  30497  wwlkm1edg  30505  2wlksot  30524  2spthsot  30525  el2wlkonot  30526  el2spthonot  30527  el2spthonot0  30528  2wlkonot3v  30532  2spthonot3v  30533  el2wlksoton  30535  el2spthsoton  30536  el2wlksotot  30539  usg2spthonot  30545  usg2spthonot0  30546  isclwlk0  30557  clwlkswlks  30561  clwwlk  30567  isclwwlk  30569  isclwwlkn  30570  clwwlkprop  30571  clwwlknprop  30573  clwlkisclwwlklem2a4  30584  clwlkisclwwlk  30589  clwwlkel  30593  clwwlkf  30594  clwwlkvbij  30601  clwwlkext2edg  30602  wwlkext2clwwlk  30603  wwlksubclwwlk  30604  clwwisshclwwlem  30608  clwwnisshclwwn  30611  erclwwlksym0  30616  erclwwlktr0  30617  eleclclwwlknlem2  30629  erclwwlkneqlen  30636  erclwwlknsym  30638  erclwwlkntr  30639  usghashecclwwlk  30647  clwlkfclwwlk1hash  30653  wwlkextproplem1  30698  rusgranumwlklem1  30705  rusgranumwlklem3  30707  rusgranumwlkb0  30709  rusgra0edg  30711  frgrancvvdeqlem3  30763  usg2spot2nb  30796  usgreg2spot  30798  2spotmdisj  30799  extwwlkfablem2lem  30806  extwwlkfablem2  30809  numclwwlkun  30810  numclwwlkovfel2  30814  numclwwlkovgel  30819  extwwlkfab  30821  numclwlk1lem2f  30823  numclwwlk2lem1  30833  numclwlk2lem2f  30834  numclwlk2lem2f1o  30836  opeliun2xp  30858  cbvmpt2x2  30864  fsuppmapnn0fiub  30937  assamulgscmlem2  30965  ply1sclrmsm  30971  smon1ply1  30983  lply1binomsc  30998  scmatscmid  31011  scmatscmidr  31012  mpt2matmul  31016  mat0dim0  31017  mat0dimid  31018  mat0dimscm  31019  mat1dimelbas  31021  lcoval  31053  lindslinindsimp1  31098  lindslinindsimp2  31104  lmod1  31141  pmatcoe1fsupp  31167  cpmatpmat  31173  cpmatel  31174  cpmatacl  31179  cpmatinvcl  31180  mat2pmatghm  31193  mat2pmatmul  31194  pmatcollpw1dstlem1  31227  monmatcollpw  31236  pmatcollpw3lem  31237  pmatcollpw3  31238  pmatcollpw3fi  31239  pmatcollpw4fi1lem1  31242  pmatcollpwscmatlem1  31245  pmatcollpwscmatlem2  31246  pmatcollpwscmatlem3  31247  pmattomply1rn  31257  mp2pm2mp  31266  monmat2matmon  31278  chfacfscmul0  31312  chfacfscmulgsum  31314  chfacfpmmulgsum  31318  cayhamlem1  31320  cpmidpmatlem2  31325  cpmidpmatlem3  31326  cpmadugsumlemB  31328  cpmadugsumlemC  31329  cpmadugsumlemF  31330  cayhamlem2  31339  bnj945  32067  bnj1400  32129  bnj18eq1  32220  bnj916  32226  bnj1014  32253  bnj1015  32254  bnj1110  32273  bnj1417  32332  bj-projeq  32785  bj-projval  32789  bj-eldiag  32832  islshp  32930  islsat  32942  lcvfbr  32971  islfl  33011  ellkr  33040  islshpkrN  33071  ldual1dim  33117  isopos  33131  cmtfvalN  33161  cvrfval  33219  isat  33237  islln  33456  islpln  33480  islvol  33523  isline  33689  ispointN  33692  ispsubsp  33695  elpmap  33708  elpmapat  33714  elpadd  33749  paddclN  33792  elpclN  33842  elpcliN  33843  pclfinN  33850  pclcmpatN  33851  ispsubclN  33887  iswatN  33944  islhp  33946  islaut  34033  ispautN  34049  isldil  34060  isltrn  34069  isdilN  34104  istrnN  34107  istendo  34710  dvhb1dimN  34936  erng1lem  34937  erngdvlem4-rN  34949  diaelval  34984  diaeldm  34987  dia1dimid  35014  cdlemm10N  35069  dibopelvalN  35094  dibopelval2  35096  dibelval3  35098  dibelval1st  35100  dibelval2nd  35103  dibeldmN  35109  dibvalrel  35114  dibglbN  35117  dicffval  35125  dicfval  35126  dicopelval  35128  dicelvalN  35129  dicelval3  35131  dicvalrelN  35136  dicelval1sta  35138  diclspsn  35145  dihopelvalbN  35189  dihopelvalcqat  35197  dihopelvalcpre  35199  dihvalrel  35230  dih1  35237  dihmeetlem4preN  35257  dihmeetlem13N  35270  dih1dimatlem  35280  dochnel2  35343  dihjatcclem4  35372  dvh2dim  35396  dvh3dim  35397  dvh4dimN  35398  dochfln0  35428  lpolsetN  35433  islpolN  35434  lcfrvalsnN  35492  lcfrlem21  35514  lcfrlem27  35520  lcfrlem37  35530  lcfr  35536  lcdlss  35570  mapdcv  35611  hdmap1fval  35748  hdmapffval  35780  hdmapfval  35781  hdmapval  35782  hgmapffval  35839  hgmapfval  35840  hdmapellkr  35868  hlhilhillem  35914
  Copyright terms: Public domain W3C validator