Theorem breq1 5111

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq1	⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 4837	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2847	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 5109	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 5109	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  ⟨cop 4594   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  breq12  5113  breq1i  5115  breq1d  5118  nbrne2  5130  brab1  5158  pocl  5576  swopolem  5578  swopo  5579  po2ne  5584  solin  5595  sotrieq  5599  sotr2  5602  isso2i  5605  somo  5607  dffr2  5621  frc  5623  frirr  5636  fr2nr  5637  wereu2  5657  vtoclr  5723  frsn  5748  brcog  5851  brcogw  5853  brcnvg  5864  dfdmf  5885  eldmg  5887  dmun  5899  dm0rn0  5913  dfrnf  5939  dmcosseq  5967  dmcosseqOLD  5968  dfres2  6042  imasng  6085  cotrg  6110  cnvsym  6113  asymref2  6116  sotri2  6128  somin1  6132  rnco  6252  coi1  6263  predtrss  6323  frpomin  6341  dffun2  6546  dffun6f  6551  funmo  6552  fun11  6610  fveq2  6881  eliman0  6918  nfunsn  6920  dffv2  6976  fvopab5  7023  dff3  7095  f1ompt  7106  fmptco  7125  dff13  7252  foeqcnvco  7298  isorel  7324  soisores  7325  soisoi  7326  isocnv  7328  isotr  7334  isomin  7335  isoini  7336  isopolem  7343  isosolem  7345  f1oiso  7349  f1oiso2  7350  weniso  7354  eqfunresadj  7360  caovordig  7617  caovordg  7619  caovord3d  7622  caovord  7623  caovord3  7625  caofrss  7715  caoftrn  7717  fr3nr  7769  dfwe2  7771  f1oweALT  7967  frxp  8120  poxp  8122  fnse  8127  poxp2  8137  frxp2  8138  poxp3  8144  frxp3  8145  xpord3pred  8146  poseq  8152  brtpos2  8226  rntpos  8233  tpostpos  8240  frrlem12  8292  ertr  8708  ecopovsym  8815  ecopovtrn  8816  isfi  8970  en0  9013  en0ALT  9014  en1  9019  endisj  9050  xpcomco  9053  sbth  9083  2pwne  9119  disjenex  9121  ssenen  9137  findcard  9146  findcard2  9147  pssnn  9151  sbthfi  9181  nneneq  9188  php  9189  onomeneq  9196  sdom1  9208  1sdom2dom  9212  isinf  9223  fineqvlem  9224  en1eqsnbi  9234  findcard3  9241  frfi  9243  fiint  9284  mapfienlem1  9363  mapfienlem2  9364  mapfienlem3  9365  mapfien  9366  marypha1lem  9391  supmo  9410  eqsup  9414  supub  9417  suplub  9418  suppr  9430  supisolem  9432  supisoex  9433  infmin  9454  infmo  9455  fiinfg  9459  fiinf2g  9460  infpr  9463  ordtypecbv  9477  ordtypelem3  9480  ordtypelem6  9483  ordtypelem7  9484  ordtypelem9  9486  ordtypelem10  9487  hartogslem1  9502  hartogs  9504  wemaplem1  9506  wemaplem2  9507  wemapso2lem  9512  card2on  9514  card2inf  9515  elharval  9521  brwdom2  9533  wdomtr  9535  cantnfs  9633  cantnfp1lem2  9646  oemapso  9649  cantnflem1  9656  wemapwe  9664  ttrclss  9687  r111  9745  kardexOLD  9885  karden  9886  kardenOLD  9887  isnumi  9939  tskwe  9943  cardid2  9946  cardonle  9950  cardne  9958  iscard2  9969  infxpenlem  10004  fodomfi2  10051  wdomfil  10052  wdomnumr  10055  alephsuc2  10071  infenaleph  10082  iunfictbso  10105  infpss  10206  cff1  10248  cfslb2n  10258  sornom  10267  fin4i  10288  isfin6  10290  isfin7  10291  isfin1-3  10376  fin1a2lem9  10398  fin1a2lem11  10400  hsmexlem4  10419  axcc2lem  10426  axcc4dom  10431  domtriomlem  10432  numthcor  10484  zorn2lem2  10487  zorn2lem3  10488  zorn2lem7  10492  zorn2g  10493  axdclem  10509  axdc  10511  brdom7disj  10521  brdom6disj  10522  uniimadom  10534  ondomon  10553  alephval2  10563  alephreg  10573  pwcfsdom  10574  elgch  10613  gchi  10615  fpwwe2lem11  10632  fpwwe2lem12  10633  winainflem  10684  winalim2  10687  tsken  10745  0tsk  10746  inar1  10766  tskord  10771  tskuni  10774  grudomon  10808  pinq  10918  nqereu  10920  enqeq  10925  ltbtwnnq  10969  ltrnq  10970  prcdnq  10984  prnmax  10986  genpnmax  10998  nqpr  11005  1idpr  11020  reclem2pr  11039  reclem3pr  11040  reclem4pr  11041  recexpr  11042  supexpr  11045  ltsosr  11085  1ne0sr  11087  ltasr  11091  supsrlem  11102  axpre-lttri  11156  axpre-lttrn  11157  axpre-ltadd  11158  axpre-sup  11160  lelttr  11306  dedekind  11379  dedekindle  11380  ltordlem  11745  lt0ne0d  11785  fimaxre3  12167  fiminre2  12169  lbreu  12171  lble  12173  sup2  12177  infm3  12180  suprleub  12187  supaddc  12188  supadd  12189  supmul1  12190  supmullem1  12191  supmul  12193  nnne0  12276  nnsub  12286  nominpos  12487  nnunb  12506  arch  12507  nn0sub  12560  nn0n0n1ge2b  12579  nn0lt10b  12664  zextle  12675  peano5uzti  12692  fzind  12700  btwnz  12705  uzval  12870  uzwo  12941  nnwof  12944  ublbneg  12963  lbzbi  12966  zsupss  12967  uzsupss  12970  uzwo3  12973  zmax  12975  rebtwnz  12977  rpnnen1lem3  13009  xrltnsym  13168  xrlttri  13170  xrlttr  13171  xrlelttr  13187  nltpnft  13196  xrmaxlt  13213  xrmaxle  13215  qbtwnre  13231  qbtwnxr  13232  xltnegi  13248  xnn0lenn0nn0  13277  xsubge0  13293  xlesubadd  13295  xmullem2  13297  xlemul1a  13320  xrinfmexpnf  13338  xrsupsslem  13339  xrinfmsslem  13340  xrub  13344  supxrunb1  13351  supxrunb2  13352  reltre  13373  rpltrp  13374  reltxrnmnf  13375  ixxval  13386  elixx1  13387  elioo2  13419  iccid  13423  icc0  13426  fzval  13543  elfz1  13546  elfznelfzo  13809  elfznelfzob  13810  flval  13834  fllelt  13837  flflp1  13847  flval2  13854  flval3  13855  flbi  13856  dfceil2  13879  ceilval2  13880  fleqceilz  13894  modid2  13938  addmodlteq  13989  fsequb2  14019  ssnn0fi  14028  seqf1olem2  14085  sqlecan  14252  faclbnd4lem1  14336  hashsnle1  14461  pr2pwpr  14523  hash3tpde  14537  rtrclreclem3  15104  relexpindlem  15107  sgnval  15132  sgnmulsgn  15153  01sqrexlem6  15305  01sqrex  15307  abslt  15373  absle  15374  rexanre  15405  rexico  15412  limsupgle  15535  limsupgre  15539  limsupbnd2  15541  rlim2lt  15555  rlim3  15556  ello12r  15575  ello1d  15581  elo12r  15586  rlimconst  15602  climshft  15634  rlimcn3  15648  o1rlimmul  15677  lo1le  15710  climsup  15728  caucvgrlem  15731  isumless  15906  divrcnv  15913  cvgrat  15944  rpnnen2lem10  16285  ruclem1  16293  ruclem2  16294  ruclem11  16302  ruclem12  16303  sqrt2irr  16311  absdvdsb  16338  dvdsle  16374  dvdsabseq  16377  dvdsdivcl  16380  dvdsext  16385  divalglem8  16464  divalglem9  16465  divalglem10  16466  divalgmod  16470  ndvdssub  16473  sadcaddlem  16521  gcdcllem1  16563  gcdcllem2  16564  gcdcllem3  16565  dfgcd2  16610  gcdzeq  16616  dvdssq  16631  nn0seqcvgd  16634  algcvgblem  16641  lcmval  16656  lcmdvds  16672  lcmgcdeq  16676  lcmfpr  16691  lcmf  16697  lcmftp  16700  lcmfunsnlem1  16701  lcmfunsnlem2lem1  16702  lcmfunsnlem2lem2  16703  lcmfdvdsb  16707  coprmgcdb  16713  coprmdvds1  16716  1nprm  16743  1idssfct  16744  isprm2lem  16745  isprm2  16746  dvdsprime  16751  nprm  16752  3prm  16758  dvdsprm  16768  exprmfct  16769  isprm5  16772  maxprmfct  16774  coprm  16776  prmdvdsncoprmbd  16792  ncoprmlnprm  16793  eulerthlem2  16847  phisum  16856  odzval  16857  pythagtriplem4  16885  pc2dvds  16945  pcprmpw2  16948  pcprmpw  16949  dvdsprmpweqle  16952  oddprmdvds  16969  prmpwdvds  16970  pockthg  16972  unbenlem  16974  prmreclem4  16985  prmreclem5  16986  prmreclem6  16987  1arith  16993  vdwlem6  17052  vdwlem11  17057  vdwlem13  17059  ramtlecl  17066  ramub  17079  rami  17081  ramubcl  17084  0ram  17086  ram0  17088  prmdvdsprmop  17109  prmolefac  17112  prmodvdslcmf  17113  prmgaplem2  17116  prmgaplcmlem1  17117  prmgaplcmlem2  17118  prmgaplem3  17119  prmgaplem4  17120  prmgaplem5  17121  prmgaplem6  17122  prmgapprmolem  17127  prmlem0  17171  prmlem1a  17172  imasaddfnlem  17588  imasvscafn  17597  imasleval  17601  prslem  18359  drsdir  18364  drsdirfi  18367  isdrs2  18368  posi  18379  posasymb  18381  pospropd  18387  pltval3  18399  plelttr  18404  pospo  18405  lubprop  18418  luble  18419  lublecllem  18420  glbprop  18431  joinval2lem  18440  joinlem  18443  meetlem  18457  meetle  18460  poslubmo  18471  posglbmo  18472  poslubd  18473  tleile  18481  latnlej  18518  isglbd  18571  lubub  18573  lubun  18577  clatleglb  18580  tsrlin  18647  letsr  18655  dirge  18665  pmtrval  19527  pmtrrn  19533  pmtrfrn  19534  pmtrrn2  19536  pmtrsn  19595  mndodcongi  19619  odeq  19626  odmulgeq  19633  gexnnod  19664  sylow1lem1  19674  pgpssslw  19690  sylow2a  19695  efgredeu  19828  efgred2  19829  gexex  19929  frgpnabllem2  19950  cyggenod  19960  dprdval  20081  dprdw  20088  dprdwd  20089  ablfacrplem  20143  ablfac1c  20149  ablfac1eu  20151  ablfaclem3  20165  omndadd  20204  abvtrivd  20946  zringlpir  21628  prmirredlem  21633  znleval  21715  frlmelbas  21917  ellspd  21963  islindf4  21999  psrbagconcl  22088  psrbagleadd1  22089  gsumbagdiaglem  22092  rhmpsrlem2  22102  psrlidm  22122  psrridm  22123  psrass1  22124  psrcom  22128  mplelbas  22151  mplmonmul  22198  ltbwe  22206  mhpmulcl  22323  psdmul  22340  coe1fsupp  22385  coe1ae0  22387  coe1mul2  22441  coe1tmmul  22449  pmatcoe1fsupp  22869  chfacffsupp  23024  chfacfscmulfsupp  23027  chfacfscmulgsum  23028  chfacfpmmulfsupp  23031  chfacfpmmulgsum  23032  ordtbas2  23359  ordtopn2  23363  ordtrest2lem  23371  pnfnei  23388  ordtt1  23547  ordthauslem  23551  2ndci  23616  2ndcsb  23617  2ndcredom  23618  2ndc1stc  23619  1stcrest  23621  2ndcctbss  23623  2ndcdisj  23624  2ndcsep  23627  lly1stc  23664  tx1stc  23818  ordthmeolem  23969  ufildom1  24094  xmetrtri2  24524  prdsxmetlem  24536  ssblex  24596  prdsbl  24659  comet  24681  stdbdxmet  24683  stdbdmopn  24686  met1stc  24689  dscmet  24740  metdstri  25020  metdscn  25025  xrhmeo  25116  bndth  25128  evth  25129  lebnumlem3  25133  pcovalg  25182  pco1  25185  pcocn  25187  pcopt  25192  pcopt2  25193  pcoass  25194  nmoleub3  25289  bcthlem5  25498  rrxfsupp  25572  minveclem4c  25595  minveclem2  25596  minveclem3b  25598  minveclem4  25602  minveclem6  25604  pmltpclem1  25618  pmltpc  25620  ovollb2lem  25658  ovolctb  25660  ovolunlem1  25667  ovoliunlem1  25672  ovoliunlem2  25673  ovoliun2  25676  ovolshftlem1  25679  ovolscalem1  25683  ovolicc1  25686  ovolicc2lem3  25689  voliunlem2  25721  voliunlem3  25722  ioombl1lem4  25731  uniioovol  25749  uniioombllem2  25753  uniioombllem3  25755  uniioombllem6  25758  volsup2  25775  ismbfd  25809  mbfsup  25834  mbflimsup  25836  itg1climres  25884  mbfi1fseqlem4  25888  itg2lr  25900  itg2leub  25904  itg2seq  25912  itg2monolem1  25920  itg2monolem3  25922  itg2mono  25923  itg2i1fseq2  25926  itg2gt0  25930  itg2cnlem1  25931  itg2cnlem2  25932  itg2cn  25933  iblss  25975  itgless  25987  ibladdlem  25990  iblabsr  26000  iblmulc2  26001  itgabs  26005  bddiblnc  26012  ditgeq1  26018  dvferm2lem  26156  rolle  26160  dvlip2  26165  c1liplem1  26166  c1lip1  26167  dvfsumlem2  26197  dvfsumlem4  26199  mdegleb  26232  degltlem1  26240  plyco0  26360  plyeq0lem  26378  coeeq2  26410  dgrle  26411  dgradd2  26436  plydiveu  26470  aareccl  26500  aalioulem2  26507  aaliou3lem7  26523  psercnlem1  26599  pilem2  26626  pilem3  26627  logltb  26776  divlogrlim  26811  logcnlem3  26820  cxpaddlelem  26927  rlimcnp  27141  cxplim  27147  cxploglim  27153  scvxcvx  27161  ftalem1  27248  ftalem2  27249  isppw2  27290  vmappw  27291  sgmnncl  27322  sqff1o  27357  fsumdvdsdiaglem  27358  dvdsppwf1o  27361  dvdsflsumcom  27363  musum  27366  muinv  27368  mpodvdsmulf1o  27369  dvdsmulf1o  27371  vmalelog  27380  vmasum  27391  logfac2  27392  perfectlem2  27405  bcmono  27452  bpos1lem  27457  bposlem9  27467  lgsmod  27498  lgsne0  27510  gausslemma2dlem4  27544  2sqlem6  27598  2sqlem8  27601  2sqlem10  27603  2sqreulem1  27621  2sqreunnlem1  27624  chtppilim  27650  rpvmasumlem  27662  dchrisumlema  27663  dchrisumlem2  27665  dchrvmasumlem1  27670  dchrvmasumiflem1  27676  dchrisum0flblem1  27683  dchrisum0flblem2  27684  dchrisum0  27695  rplogsum  27702  logsqvma  27717  pntpbnd1  27761  pntpbnd2  27762  pntibndlem3  27767  pntlemj  27778  pntlemi  27779  pntlem3  27784  pnt3  27787  ostth3  27813  nodense  27867  noresle  27872  nosupprefixmo  27875  noinfprefixmo  27876  nosupcbv  27877  nosupdm  27879  nosupbnd1lem1  27883  nosupbnd1lem4  27886  nosupbnd1  27889  nosupbnd2lem1  27890  nosupbnd2  27891  noinfcbv  27892  noinfdm  27894  noinffv  27896  noinfres  27897  noinfbnd1lem3  27900  noinfbnd1lem4  27901  noinfbnd1lem5  27902  noinfbnd1  27904  noetalem2  27917  nocvxminlem  27958  sltssnb  27973  sltssepc  27975  conway  27983  cutsval  27984  etaslts  27997  lesrec  28003  eqcuts3  28008  bday1  28018  cuteq1  28021  madeval2  28037  rightval  28054  elleft  28055  sltsright  28065  made0  28067  madecut  28087  left1s  28099  madebdaylemlrcut  28103  ltslpss  28112  cofslts  28122  coinitslts  28123  cofcutr  28128  cofcutrtime  28131  cofss  28134  coiniss  28135  cutmax  28138  cutmin  28139  cutminmax  28140  addsproplem1  28173  addsprop  28180  leadds1  28193  addsuniflem  28205  negsproplem1  28232  negsprop  28239  negsid  28245  negsunif  28259  mulsproplemcbv  28319  mulsproplem1  28320  mulsproplem9  28328  mulsprop  28334  sltmuls1  28351  sltmuls2  28352  mulsuniflem  28353  precsexlem11  28421  abslts  28453  oncutlt  28468  oniso  28475  bdayons  28480  addonbday  28483  n0fincut  28559  onsfi  28560  n0subs  28567  bdayn0p1  28573  eucliddivs  28580  zcuts  28611  twocut  28627  halfcut  28662  addhalfcut  28663  bdaypw2n0bndlem  28667  bdayfinbndcbv  28670  bdayfinbndlem1  28671  bdayfinbndlem2  28672  z12bdaylem1  28674  elreno  28695  elreno2  28699  tgjustc1  28755  tgjustc2  28756  iscgrglt  28794  tgcgr4  28811  hlcgreu  28901  elplng  29073  plngcplem  29078  lmif  29105  islmib  29107  trgcopyeu  29128  iscgrad  29133  inaghl  29173  axlowdim2  29321  axlowdim  29322  axcontlem2  29326  axcontlem3  29327  axcontlem4  29328  axcontlem7  29331  axcontlem9  29333  axcontlem10  29334  axcontlem11  29335  axcontlem12  29336  ebtwntg  29343  umgrupgr  29464  nbusgrvtxm1  29740  crctcshwlkn0lem2  30171  crctcshwlkn0lem3  30172  crctcsh  30184  wlkswwlksf1o  30239  clwlkclwwlklem2fv1  30357  clwlkclwwlkf  30370  0clwlkv  30493  eupth2  30601  numclwwlk5  30750  nmoubi  31135  minvecolem2  31238  minvecolem3  31239  minvecolem4c  31242  minvecolem4  31243  minvecolem5  31244  minvecolem6  31245  htthlem  31280  chlimi  31597  chcompl  31605  hsn0elch  31611  cmbr3  31971  cmcm  31977  cmcm3  31978  lecm  31980  nmopub  32271  nmfnleub  32288  nmopun  32377  nmcexi  32389  cnlnadjlem7  32436  pjnmopi  32511  stle0i  32602  stlesi  32604  stm1i  32606  csmdsymi  32697  cvmd  32699  atcveq0  32711  atcv1  32743  atord  32751  atcvat2  32752  chirred  32758  mdsym  32775  mddmdin0i  32794  cdj1i  32796  fmptcof2  33013  fnpreimac  33026  isoun  33058  fcobijfs  33077  fcobijfs2  33078  lt2addrd  33106  xlt2addrd  33115  xrge0infss  33116  infxrge0glb  33121  xrofsup  33123  fz1nnct  33157  toslublem  33301  tosglblem  33303  ismntd  33313  mgccole1  33319  mgccole2  33320  mgcmnt1  33321  mgcmnt2  33322  dfmgc2lem  33324  dfmgc2  33325  psgnfzto1stlem  33429  fzto1st  33432  psgnfzto1st  33434  trsp2cyc  33452  xrnarchi  33513  archirng  33517  archiexdiv  33519  archiabl  33527  isarchiofld  33528  elrgspnlem1  33571  elrgspnlem2  33572  elrgspnlem3  33573  elrgspnlem4  33574  elrgspn  33575  elrgspnsubrunlem1  33576  elrgspnsubrunlem2  33577  elrgspnsubrun  33578  linds2eq  33703  elrspunidl  33745  elrspunsn  33746  isrprm  33816  evl1deg1  33875  evl1deg2  33876  evl1deg3  33877  0mplrim  33913  selvply1rhmlema  33917  selvply1rhmlemb  33918  selvply1rhmlem1  33919  selvply1rhmlem2  33920  selvply1rhmlem4  33922  selvply1rhm0  33925  extvfvvcl  33934  extvfvcl  33935  mplmulmvr  33938  evlextv  33941  mplvrpmlem  33942  mplvrpmfgalem  33943  mplvrpmga  33944  mplvrpmmhm  33945  mplvrpmrhm  33946  psrmonmul  33949  psrmonprod  33951  esplyfval0  33963  esplylem  33965  esplyfv1  33968  esplyfval3  33971  esplyfvaln  33973  esplyind  33974  ply1degltdimlem  34021  lbsdiflsp0  34025  fedgmullem1  34028  fedgmullem2  34029  fedgmul  34030  fldextrspunlsplem  34072  fldextrspunlsp  34073  smatrcl  34195  smatlem  34196  madjusmdetlem2  34227  madjusmdet  34230  cmpcref  34249  ldlfcntref  34253  dispcmp  34258  zarcmplem  34280  ordtrest2NEWlem  34321  ordtconnlem1  34323  xrge0iifiso  34334  rge0scvg  34348  gsumesum  34458  esumfsup  34469  esumpinfval  34472  esumpcvgval  34477  esumcvg  34485  sigaclcu  34516  sigaclci  34531  unelsiga  34533  unelldsys  34557  sigapildsys  34561  ldgenpisyslem1  34562  fiunelros  34573  measvun  34608  voliune  34628  volfiniune  34629  oms0  34696  omssubaddlem  34698  omssubadd  34699  carsgsigalem  34714  carsgclctunlem2  34718  carsgclctun  34720  pmeasmono  34723  pmeasadd  34724  orvcval2  34858  dstfrvel  34873  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemsv  34909  ballotlemsf1o  34913  breprexp  35029  tgoldbachgt  35059  bnj23  35116  bnj1185  35190  bnj1152  35395  bnj1418  35437  fnrelpredd  35491  kardval2  35574  elkarden  35576  kardeng  35578  kardnnfi  35590  rankkardu  35592  loop1cycl  35637  umgr2cycl  35641  acycgrcycl  35647  dfdm5  36273  dfrn5  36274  wzel  36322  wsuclem  36323  brpprod  36383  brsset  36387  brbigcup  36396  dffix2  36403  elfuns  36413  brimageg  36425  brdomaing  36433  brrangeg  36434  brimg  36435  brapply  36436  lemsuccf  36439  funpartlem  36442  brrestrict  36449  dfrecs2  36450  dfrdg4  36451  brofs  36505  btwncomim  36513  btwnintr  36519  btwnexch3  36520  btwnexch2  36523  brifs  36543  brcolinear2  36558  colineardim1  36561  brfs  36579  btwnconn1  36601  segcon2  36605  seglerflx  36612  seglemin  36613  btwnsegle  36617  colinbtwnle  36618  broutsideof2  36622  fvray  36641  lineunray  36647  lineelsb2  36648  linerflx1  36649  trer  36855  elicc3  36856  finminlem  36857  nn0prpwlem  36861  nn0prpw  36862  fnessref  36896  refssfne  36897  weiunlem  37002  weiunfrlem  37003  weiunfr  37006  weiunse  37007  unblimceq0lem  37123  unblimceq0  37124  unbdqndv2  37128  knoppndvlem21  37149  taupilemrplb  37992  dfgcd3  37996  icorempo  38025  icoreval  38027  iooelexlt  38036  relowlssretop  38037  domalom  38078  ctbssinf  38080  pibt2  38091  phpreu  38283  fin2solem  38285  fin2so  38286  ltflcei  38287  ptrecube  38299  poimirlem1  38300  poimirlem2  38301  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem9  38308  poimirlem12  38311  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  poimirlem26  38325  poimirlem27  38326  poimirlem32  38331  heicant  38334  mblfinlem1  38336  mblfinlem2  38337  itg2addnclem  38350  itg2addnclem3  38352  itg2addnc  38353  itg2gt0cn  38354  ibladdnclem  38355  iblmulc2nc  38364  itgabsnc  38368  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  indexdom  38413  filbcmb  38419  fdc  38424  prdsbnd  38472  heiborlem3  38492  rrnequiv  38514  rngoueqz  38619  eqbrtr  38915  elrnressn  38957  inxprnres  38975  presucmap  39172  eqvreltr  39368  prtlem10  39667  lsatcveq0  39834  lsatcv1  39850  oposlem  39984  opnlen0  39990  lub0N  39991  glb0N  39995  omllaw  40045  cmtbr4N  40057  cvrval  40071  cvrnbtwn  40073  cvrnbtwn2  40077  cvrnbtwn3  40078  cvrcon3b  40079  cvrnbtwn4  40081  atcvreq0  40116  atnle  40119  atlatmstc  40121  cvlexch1  40130  glbconN  40179  hlsuprexch  40183  exatleN  40206  cvratlem  40223  atcvrj0  40230  atcvrj2b  40234  atlelt  40240  cvrat4  40245  3dim1lem5  40268  3dim2  40270  3dim3  40271  ps-2  40280  llni  40310  llnn0  40318  llnle  40320  lplni  40334  lplni2  40339  lplnle  40342  lplnn0N  40349  llncvrlpln  40360  2llnjN  40369  lvoli  40377  lvoli3  40379  lvoli2  40383  lvoln0N  40393  4at  40415  lplncvrlvol  40418  2lplnj  40422  dalemcea  40462  dalem3  40466  psubspi  40549  linepsubN  40554  elpmap  40560  pmapsub  40570  lnatexN  40581  cdlema1N  40593  cdlemb  40596  elpadd  40601  paddvaln0N  40603  paddasslem5  40626  llnexchb2lem  40670  llnexch2N  40672  islhp  40798  lhpat3  40848  4atexlemex2  40873  4atex  40878  4atex2-0aOLDN  40880  4atex2-0cOLDN  40882  lautle  40886  lautcvr  40894  lauteq  40897  ldilval  40915  ltrnu  40923  trlval2  40965  trlne  40987  cdleme0ex1N  41025  cdleme0nex  41092  cdleme18d  41097  cdlemednuN  41102  cdleme25b  41156  cdleme25cv  41160  cdleme27b  41170  cdleme29b  41177  cdleme31sn  41182  cdleme31fv  41192  cdleme31fv2  41195  cdlemefrs29bpre0  41198  cdlemefr29bpre0N  41208  cdlemefr29clN  41209  cdlemefr32fvaN  41211  cdlemefr32fva1  41212  cdlemefs29pre00N  41214  cdlemefs32sn1aw  41216  cdlemefs29bpre0N  41218  cdlemefs29bpre1N  41219  cdlemefs29cpre1N  41220  cdlemefs29clN  41221  cdlemefs32fvaN  41224  cdlemefs32fva1  41225  cdleme41sn3a  41235  cdleme32fva  41239  cdleme32e  41247  cdleme35f  41256  cdleme40v  41271  cdleme42b  41280  trlord  41371  cdlemg1cex  41390  diaval  41834  diaeldm  41838  diaelrnN  41847  cdlemm10N  41920  dibglbN  41968  dicval  41978  dicfnN  41985  dicvalrelN  41987  dihval  42034  dihlsscpre  42036  dihglblem3N  42097  dihmeetlem2N  42101  djhcvat42  42217  lcmineqlem4  42827  aks4d1p4  42874  aks4d1p5  42875  aks4d1p7  42878  aks4d1p8d2  42880  aks4d1p8  42882  hashnexinjle  42924  sticksstones1  42941  sticksstones2  42942  sticksstones10  42950  sticksstones12a  42952  aks6d1c7lem4  42978  aks6d1c7  42979  grpods  42989  unitscyglem2  42991  unitscyglem3  42992  unitscyglem4  42993  qsalrel  43037  supinf  43038  dvdsexpnn0  43123  redvmptabs  43149  sn-nnne0  43262  sn-sup2  43293  fimgmcyclem  43329  flt4lem2  43407  flt4lem7  43419  lzenom  43529  fphpdo  43572  irrapxlem4  43580  pellexlem6  43589  infmrgelbi  43633  pellfundre  43636  pellfundlb  43639  monotoddzz  43698  zindbi  43701  jm2.27  43763  rmydioph  43769  rpnnen3lem  43786  fnwe2lem2  43806  aomclem8  43816  hbtlem5  43883  hbt  43885  sdomne0  44167  sdomne0d  44168  ensucne0  44283  sucomisnotcard  44298  en2pr  44301  pr2cv  44302  refimssco  44361  rfovfvfvd  44757  rfovcnvf1od  44758  fsovrfovd  44763  nzss  45055  relprel  45688  permaxinf2lem  45749  wessf1ornlem  45931  axccdom  45966  dmrelrnrel  45970  axccd  45972  rnmptlb  45986  rnmptbdd  45988  rnmptbd2  45992  rnmptbdlem  45998  rnmptbd  45999  dstregt0  46029  suplesup  46083  supxrunb3  46142  supxrleubrnmpt  46148  rexabslelem  46160  rexabsle  46161  suprleubrnmpt  46164  infrnmptle  46165  infxrunb3rnmpt  46170  infxrpnf  46188  supminfxr  46206  infrpgernmpt  46207  xrpnf  46227  limsupre  46383  limsupref  46427  limsupbnd1f  46428  limsuppnfd  46444  climinf2  46449  limsuppnf  46453  climinfmpt  46457  climinf3  46458  limsupmnflem  46462  limsupmnf  46463  limsupre2  46467  limsupmnfuzlem  46468  limsupre2mpt  46472  limsupre3lem  46474  limsupre3  46475  limsupre3mpt  46476  limsupre3uzlem  46477  limsupre3uz  46478  limsupreuz  46479  limsupreuzmpt  46481  liminfval2  46510  liminfreuzlem  46544  liminfreuz  46545  xlimpnfxnegmnf  46556  cnrefiisplem  46571  xlimpnfv  46580  xlimpnf  46584  xlimpnfmpt  46586  dfxlim2  46590  icccncfext  46629  cncficcgt0  46630  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  stoweidlem5  46747  stoweidlem20  46762  stoweidlem26  46768  stoweidlem28  46770  stoweidlem29  46771  stoweidlem34  46776  wallispilem3  46809  stirlinglem13  46828  fourierdlem41  46890  fourierdlem42  46891  fourierdlem51  46899  fourierdlem54  46902  salunicl  47058  saluncl  47059  salexct  47076  salexct2  47081  salexct3  47084  salgencntex  47085  salgensscntex  47086  sge0pnffigt  47138  meadjuni  47199  omeunile  47247  ovnlerp  47304  hoidifhspval  47350  ovolval5lem2  47395  salpreimagelt  47449  pimincfltioo  47460  salpreimagtge  47467  salpreimagtlt  47472  incsmf  47484  issmfgt  47498  smfpreimagt  47504  decsmf  47509  issmfge  47512  smfpimgtxr  47522  smfpreimage  47524  smfinflem  47559  smfinf  47560  finfdm  47588  funressnfv  47808  funressnvmo  47810  funressnmo  47811  dfdfat2  47893  tz6.12-afv  47938  funressndmafv2rn  47988  tz6.12-afv2  48005  dfatcolem  48020  dfatco  48021  zplusmodne  48114  m1modne  48119  minusmod5ne  48120  submodneaddmod  48122  modmknepk  48133  iccpartigtl  48200  iccpartgt  48204  icceuelpartlem  48212  iccpartnel  48215  sprsymrelfolem2  48270  nprmmul2  48305  goldbachthlem2  48326  odz2prm2pw  48343  fmtnoprmfac1  48345  fmtnoprmfac2  48347  fmtnofac2  48349  fmtno4prmfac  48352  fmtno4prm  48355  prmdvdsfmtnof1lem1  48364  31prm  48377  nprmdvdsfacm1  48404  perfectALTVlem2  48515  nnsum3primes4  48581  nnsum3primesprm  48583  nnsum3primesgbe  48585  nnsum3primesle9  48587  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  wtgoldbnnsum4prm  48595  bgoldbnnsum3prm  48597  bgoldbtbndlem4  48601  bgoldbtbnd  48602  tgblthelfgott  48608  tgoldbach  48610  assintop  49002  isassintop  49003  assintopcllaw  49005  ztprmneprm  49155  ply1mulgsumlem1  49194  ply1mulgsumlem2  49195  lco0  49235  lcoel0  49236  lincsumcl  49239  lincscmcl  49240  lcoss  49244  linindslinci  49256  lindslinindsimp1  49265  linds0  49273  el0ldep  49274  lindsrng01  49276  ldepspr  49281  islindeps2  49291  isldepslvec2  49293  zlmodzxzldep  49312  ldepsnlinc  49316  elbigo2r  49361  xpco2  49663  tposres0  49683  lubsscl  49766  glbsscl  49767  lubprlem  49768  ipolub  49794  ipoglb  49797  catprslem  49816  infsubc2  49867  nelsubc3lem  49876  cnelsubclem  50409  setrec2lem1  50499