Theorem breq1 5105

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 4832	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2845	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 5103	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 5103	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ⟨cop 4589   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  breq12  5107  breq1i  5109  breq1d  5112  nbrne2  5124  brab1  5152  pocl  5563  swopolem  5565  swopo  5566  po2ne  5571  solin  5582  sotrieq  5586  sotr2  5589  isso2i  5592  somo  5594  dffr2  5608  frc  5610  frirr  5623  fr2nr  5624  wereu2  5644  vtoclr  5710  frsn  5735  brcog  5840  brcogw  5842  brcnvg  5853  dfdmf  5874  eldmg  5876  dmun  5888  dm0rn0  5902  dfrnf  5928  dmcosseq  5956  dmcosseqOLD  5957  dfres2  6031  imasng  6074  cotrg  6099  cnvsym  6102  asymref2  6105  sotri2  6117  somin1  6121  rnco  6242  coi1  6253  predtrss  6314  frpomin  6332  dffun2  6537  dffun6f  6542  funmo  6543  fun11  6602  fveq2  6873  eliman0  6910  nfunsn  6912  dffv2  6968  fvopab5  7015  dff3  7088  f1ompt  7099  fmptco  7118  dff13  7246  foeqcnvco  7296  isorel  7322  soisores  7323  soisoi  7324  isocnv  7326  isotr  7332  isomin  7333  isoini  7334  isopolem  7341  isosolem  7343  f1oiso  7347  f1oiso2  7348  weniso  7352  eqfunresadj  7358  caovordig  7614  caovordg  7616  caovord3d  7619  caovord  7620  caovord3  7622  caofrss  7715  caoftrn  7717  fr3nr  7769  dfwe2  7771  f1oweALT  7967  frxp  8121  poxp  8123  fnse  8128  poxp2  8138  frxp2  8139  poxp3  8145  frxp3  8146  xpord3pred  8147  poseq  8153  brtpos2  8227  rntpos  8234  tpostpos  8241  frrlem12  8293  ertr  8711  ecopovsym  8818  ecopovtrn  8819  isfi  8980  en0  9023  en0ALT  9024  en1  9029  endisj  9061  xpcomco  9064  sbth  9094  2pwne  9130  disjenex  9132  ssenen  9148  findcard  9157  findcard2  9158  pssnn  9162  sbthfi  9192  nneneq  9199  php  9200  onomeneq  9207  sdom1  9219  1sdom2dom  9223  isinf  9234  fineqvlem  9235  en1eqsnbi  9245  findcard3  9252  frfi  9254  fiint  9296  mapfienlem1  9375  mapfienlem2  9376  mapfienlem3  9377  mapfien  9378  marypha1lem  9403  supmo  9422  eqsup  9426  supub  9429  suplub  9430  suppr  9442  supisolem  9444  supisoex  9445  infmin  9466  infmo  9467  fiinfg  9471  fiinf2g  9472  infpr  9475  ordtypecbv  9489  ordtypelem3  9492  ordtypelem6  9495  ordtypelem7  9496  ordtypelem9  9498  ordtypelem10  9499  hartogslem1  9514  hartogs  9516  wemaplem1  9518  wemaplem2  9519  wemapso2lem  9524  card2on  9526  card2inf  9527  elharval  9533  brwdom2  9545  wdomtr  9547  cantnfs  9645  cantnfp1lem2  9658  oemapso  9661  cantnflem1  9668  wemapwe  9676  ttrclss  9699  r111  9757  kardexOLD  9929  karden  9930  kardenOLD  9931  setrec2lem1  9945  isnumi  9998  tskwe  10002  cardid2  10005  cardonle  10009  cardne  10017  iscard2  10028  infxpenlem  10063  fodomfi2  10110  wdomfil  10111  wdomnumr  10114  alephsuc2  10130  infenaleph  10141  iunfictbso  10164  infpss  10265  cff1  10307  cfslb2n  10317  sornom  10326  fin4i  10347  isfin6  10349  isfin7  10350  isfin1-3  10435  fin1a2lem9  10457  fin1a2lem11  10459  hsmexlem4  10478  axcc2lem  10485  axcc4dom  10490  domtriomlem  10491  numthcor  10543  zorn2lem2  10546  zorn2lem3  10547  zorn2lem7  10551  zorn2g  10552  axdclem  10568  axdc  10570  brdom7disj  10581  brdom6disj  10582  uniimadom  10599  ondomon  10618  alephval2  10628  alephreg  10638  pwcfsdom  10639  elgch  10678  gchi  10680  fpwwe2lem11  10697  fpwwe2lem12  10698  winainflem  10749  winalim2  10752  tsken  10810  0tsk  10811  inar1  10831  tskord  10836  tskuni  10839  grudomon  10873  pinq  10983  nqereu  10985  enqeq  10990  ltbtwnnq  11034  ltrnq  11035  prcdnq  11049  prnmax  11051  genpnmax  11063  nqpr  11070  1idpr  11085  reclem2pr  11104  reclem3pr  11105  reclem4pr  11106  recexpr  11107  supexpr  11110  ltsosr  11150  1ne0sr  11152  ltasr  11156  supsrlem  11167  axpre-lttri  11221  axpre-lttrn  11222  axpre-ltadd  11223  axpre-sup  11225  lelttr  11371  dedekind  11444  dedekindle  11445  ltordlem  11810  lt0ne0d  11850  fimaxre3  12232  fiminre2  12234  lbreu  12236  lble  12238  sup2  12242  infm3  12245  suprleub  12252  supaddc  12253  supadd  12254  supmul1  12255  supmullem1  12256  supmul  12258  nnne0  12341  nnsub  12351  nominpos  12552  nnunb  12571  arch  12572  nn0sub  12625  nn0n0n1ge2b  12644  nn0lt10b  12730  zextle  12741  peano5uzti  12758  fzind  12766  btwnz  12771  uzval  12936  uzwo  13007  nnwof  13010  ublbneg  13029  lbzbi  13032  zsupss  13033  uzsupss  13036  uzwo3  13039  zmax  13041  rebtwnz  13043  rpnnen1lem3  13076  xrltnsym  13235  xrlttri  13237  xrlttr  13238  xrlelttr  13254  nltpnft  13263  xrmaxlt  13280  xrmaxle  13282  qbtwnre  13298  qbtwnxr  13299  xltnegi  13315  xnn0lenn0nn0  13344  xsubge0  13360  xlesubadd  13362  xmullem2  13364  xlemul1a  13387  xrinfmexpnf  13405  xrsupsslem  13406  xrinfmsslem  13407  xrub  13411  supxrunb1  13418  supxrunb2  13419  reltre  13440  rpltrp  13441  reltxrnmnf  13442  ixxval  13453  elixx1  13454  elioo2  13486  iccid  13490  icc0  13493  fzval  13610  elfz1  13613  elfznelfzo  13876  elfznelfzob  13877  flval  13902  fllelt  13905  flflp1  13915  flval2  13922  flval3  13923  flbi  13924  dfceil2  13947  ceilval2  13948  fleqceilz  13962  modid2  14006  addmodlteq  14057  fsequb2  14087  ssnn0fi  14096  seqf1olem2  14153  sqlecan  14320  faclbnd4lem1  14404  hashsnle1  14529  pr2pwpr  14591  hash3tpde  14605  rtrclreclem3  15180  relexpindlem  15183  sgnval  15208  sgnmulsgn  15229  01sqrexlem6  15381  01sqrex  15383  abslt  15449  absle  15450  rexanre  15481  rexico  15488  limsupgle  15611  limsupgre  15615  limsupbnd2  15617  rlim2lt  15631  rlim3  15632  ello12r  15651  ello1d  15657  elo12r  15662  rlimconst  15678  climshft  15710  rlimcn3  15724  o1rlimmul  15753  lo1le  15786  climsup  15804  caucvgrlem  15807  isumless  15981  divrcnv  15988  cvgrat  16019  rpnnen2lem10  16358  ruclem1  16366  ruclem2  16367  ruclem11  16375  ruclem12  16376  sqrt2irr  16384  absdvdsb  16411  dvdsle  16447  dvdsabseq  16450  dvdsdivcl  16453  dvdsext  16458  divalglem8  16537  divalglem9  16538  divalglem10  16539  divalgmod  16543  ndvdssub  16546  sadcaddlem  16594  gcdcllem1  16636  gcdcllem2  16637  gcdcllem3  16638  dfgcd2  16683  gcdzeq  16689  dvdssq  16704  nn0seqcvgd  16707  algcvgblem  16714  lcmval  16729  lcmdvds  16745  lcmgcdeq  16749  lcmfpr  16764  lcmf  16770  lcmftp  16773  lcmfunsnlem1  16774  lcmfunsnlem2lem1  16775  lcmfunsnlem2lem2  16776  lcmfdvdsb  16780  coprmgcdb  16786  coprmdvds1  16789  1nprm  16816  1idssfct  16817  isprm2lem  16818  isprm2  16819  dvdsprime  16824  nprm  16825  3prm  16831  dvdsprm  16841  exprmfct  16842  isprm5  16845  maxprmfct  16847  coprm  16849  prmdvdsncoprmbd  16865  ncoprmlnprm  16866  eulerthlem2  16920  phisum  16929  odzval  16930  pythagtriplem4  16958  pc2dvds  17018  pcprmpw2  17021  pcprmpw  17022  dvdsprmpweqle  17025  oddprmdvds  17042  prmpwdvds  17043  pockthg  17045  unbenlem  17047  prmreclem4  17058  prmreclem5  17059  prmreclem6  17060  1arith  17066  vdwlem6  17125  vdwlem11  17130  vdwlem13  17132  ramtlecl  17139  ramub  17152  rami  17154  ramubcl  17157  0ram  17159  ram0  17161  prmdvdsprmop  17182  prmolefac  17185  prmodvdslcmf  17186  prmgaplem2  17189  prmgaplcmlem1  17190  prmgaplcmlem2  17191  prmgaplem3  17192  prmgaplem4  17193  prmgaplem5  17194  prmgaplem6  17195  prmgapprmolem  17200  prmlem0  17244  prmlem1a  17245  imasaddfnlem  17661  imasvscafn  17670  imasleval  17674  prslem  18432  drsdir  18437  drsdirfi  18440  isdrs2  18441  posi  18452  posasymb  18454  pospropd  18460  pltval3  18472  plelttr  18477  pospo  18478  lubprop  18491  luble  18492  lublecllem  18493  glbprop  18504  joinval2lem  18513  joinlem  18516  meetlem  18530  meetle  18533  poslubmo  18544  posglbmo  18545  poslubd  18546  tleile  18554  latnlej  18591  isglbd  18644  lubub  18646  lubun  18650  clatleglb  18653  tsrlin  18720  letsr  18728  dirge  18738  pmtrval  19626  pmtrrn  19632  pmtrfrn  19633  pmtrrn2  19635  pmtrsn  19694  mndodcongi  19718  odeq  19725  odmulgeq  19732  gexnnod  19763  sylow1lem1  19773  pgpssslw  19789  sylow2a  19794  efgredeu  19927  efgred2  19928  gexex  20028  frgpnabllem2  20049  cyggenod  20059  dprdval  20180  dprdw  20187  dprdwd  20188  ablfacrplem  20242  ablfac1c  20248  ablfac1eu  20250  ablfaclem3  20264  omndadd  20303  abvtrivd  21050  zringlpir  21734  prmirredlem  21739  znleval  21821  frlmelbas  22023  ellspd  22069  islindf4  22105  psrbagconcl  22196  psrbagleadd1  22197  gsumbagdiaglem  22200  rhmpsrlem2  22210  psrlidm  22230  psrridm  22231  psrass1  22232  psrcom  22236  mplelbas  22259  mplmonmul  22306  ltbwe  22314  mhpmulcl  22431  psdmul  22448  coe1fsupp  22493  coe1ae0  22495  coe1mul2  22549  coe1tmmul  22557  pmatcoe1fsupp  22980  chfacffsupp  23135  chfacfscmulfsupp  23138  chfacfscmulgsum  23139  chfacfpmmulfsupp  23142  chfacfpmmulgsum  23143  ordtbas2  23470  ordtopn2  23474  ordtrest2lem  23482  pnfnei  23499  ordtt1  23658  ordthauslem  23662  2ndci  23727  2ndcsb  23728  2ndcredom  23729  2ndc1stc  23730  1stcrest  23732  2ndcctbss  23735  2ndcdisj  23736  2ndcsep  23739  lly1stc  23776  tx1stc  23930  ordthmeolem  24081  ufildom1  24206  xmetrtri2  24636  prdsxmetlem  24648  ssblex  24708  prdsbl  24771  comet  24793  stdbdxmet  24795  stdbdmopn  24798  met1stc  24801  dscmet  24852  metdstri  25132  metdscn  25137  xrhmeo  25228  bndth  25240  evth  25241  lebnumlem3  25245  pcovalg  25294  pco1  25297  pcocn  25299  pcopt  25304  pcopt2  25305  pcoass  25306  nmoleub3  25401  bcthlem5  25610  rrxfsupp  25684  minveclem4c  25707  minveclem2  25708  minveclem3b  25710  minveclem4  25714  minveclem6  25716  pmltpclem1  25730  pmltpc  25732  ovollb2lem  25770  ovolctb  25772  ovolunlem1  25779  ovoliunlem1  25784  ovoliunlem2  25785  ovoliun2  25788  ovolshftlem1  25791  ovolscalem1  25795  ovolicc1  25798  ovolicc2lem3  25801  voliunlem2  25833  voliunlem3  25834  ioombl1lem4  25843  uniioovol  25861  uniioombllem2  25865  uniioombllem3  25867  uniioombllem6  25870  volsup2  25887  ismbfd  25921  mbfsup  25946  mbflimsup  25948  itg1climres  25996  mbfi1fseqlem4  26000  itg2lr  26012  itg2leub  26016  itg2seq  26024  itg2monolem1  26032  itg2monolem3  26034  itg2mono  26035  itg2i1fseq2  26038  itg2gt0  26042  itg2cnlem1  26043  itg2cnlem2  26044  itg2cn  26045  iblss  26086  itgless  26098  ibladdlem  26101  iblabsr  26111  iblmulc2  26112  itgabs  26116  bddiblnc  26123  ditgeq1  26129  dvferm2lem  26267  rolle  26271  dvlip2  26276  c1liplem1  26277  c1lip1  26278  dvfsumlem2  26308  dvfsumlem4  26310  mdegleb  26343  degltlem1  26351  plyco0  26471  plyeq0lem  26490  coeeq2  26522  dgrle  26523  dgradd2  26548  plydiveu  26582  aareccl  26616  aalioulem2  26623  aaliou3lem7  26639  psercnlem1  26715  pilem2  26742  pilem3  26743  logltb  26891  divlogrlim  26926  logcnlem3  26935  cxpaddlelem  27042  rlimcnp  27256  cxplim  27262  cxploglim  27268  scvxcvx  27276  ftalem1  27363  ftalem2  27364  isppw2  27405  vmappw  27406  sgmnncl  27437  sqff1o  27472  fsumdvdsdiaglem  27473  dvdsppwf1o  27476  dvdsflsumcom  27478  musum  27481  muinv  27483  mpodvdsmulf1o  27484  dvdsmulf1o  27486  vmalelog  27495  vmasum  27506  logfac2  27507  perfectlem2  27520  bcmono  27567  bpos1lem  27572  bposlem9  27582  lgsmod  27613  lgsne0  27625  gausslemma2dlem4  27659  2sqlem6  27713  2sqlem8  27716  2sqlem10  27718  2sqreulem1  27736  2sqreunnlem1  27739  chtppilim  27765  rpvmasumlem  27777  dchrisumlema  27778  dchrisumlem2  27780  dchrvmasumlem1  27785  dchrvmasumiflem1  27791  dchrisum0flblem1  27798  dchrisum0flblem2  27799  dchrisum0  27810  rplogsum  27817  logsqvma  27832  pntpbnd1  27876  pntpbnd2  27877  pntibndlem3  27882  pntlemj  27893  pntlemi  27894  pntlem3  27899  pnt3  27902  ostth3  27928  nodense  27982  noresle  27987  nosupprefixmo  27990  noinfprefixmo  27991  nosupcbv  27992  nosupdm  27994  nosupbnd1lem1  27998  nosupbnd1lem4  28001  nosupbnd1  28004  nosupbnd2lem1  28005  nosupbnd2  28006  noinfcbv  28007  noinfdm  28009  noinffv  28011  noinfres  28012  noinfbnd1lem3  28015  noinfbnd1lem4  28016  noinfbnd1lem5  28017  noinfbnd1  28019  noetalem2  28032  nocvxminlem  28073  sltssnb  28088  sltssepc  28090  conway  28098  cutsval  28099  etaslts  28112  lesrec  28118  eqcuts3  28123  bday1  28133  cuteq1  28136  madeval2  28152  rightval  28169  elleft  28170  sltsright  28180  made0  28182  madecut  28202  left1s  28214  madebdaylemlrcut  28218  ltslpss  28227  cofslts  28237  coinitslts  28238  cofcutr  28243  cofcutrtime  28246  cofss  28249  coiniss  28250  cutmax  28253  cutmin  28254  cutminmax  28255  addsproplem1  28288  addsprop  28295  leadds1  28308  addsuniflem  28320  negsproplem1  28347  negsprop  28354  negsid  28360  negsunif  28374  mulsproplemcbv  28434  mulsproplem1  28435  mulsproplem9  28443  mulsprop  28449  sltmuls1  28466  sltmuls2  28467  mulsuniflem  28468  precsexlem11  28536  abslts  28568  oncutlt  28583  oniso  28590  bdayons  28595  addonbday  28598  n0fincut  28674  onsfi  28675  n0subs  28682  bdayn0p1  28688  eucliddivs  28695  zcuts  28726  twocut  28742  halfcut  28777  addhalfcut  28778  bdaypw2n0bndlem  28782  bdayfinbndcbv  28785  bdayfinbndlem1  28786  bdayfinbndlem2  28787  z12bdaylem1  28789  elreno  28810  elreno2  28814  tgjustc1  28870  tgjustc2  28871  iscgrglt  28910  tgcgr4  28927  hlcgreu  29017  elplng  29191  plngcplem  29196  lmif  29223  islmib  29225  trgcopyeu  29246  iscgrad  29251  inaghl  29297  axlowdim2  29471  axlowdim  29472  axcontlem2  29476  axcontlem3  29477  axcontlem4  29478  axcontlem7  29481  axcontlem9  29483  axcontlem10  29484  axcontlem11  29485  axcontlem12  29486  ebtwntg  29493  umgrupgr  29614  nbusgrvtxm1  29893  crctcshwlkn0lem2  30333  crctcshwlkn0lem3  30334  crctcsh  30346  wlkswwlksf1o  30401  clwlkclwwlklem2fv1  30519  clwlkclwwlkf  30532  0clwlkv  30655  loop1cycl  30677  umgr2cycl  30680  acycgrcycl  30686  eupth2  30773  numclwwlk5  30922  nmoubi  31307  minvecolem2  31410  minvecolem3  31411  minvecolem4c  31414  minvecolem4  31415  minvecolem5  31416  minvecolem6  31417  htthlem  31452  chlimi  31769  chcompl  31777  hsn0elch  31783  cmbr3  32143  cmcm  32149  cmcm3  32150  lecm  32152  nmopub  32443  nmfnleub  32460  nmopun  32549  nmcexi  32561  cnlnadjlem7  32608  pjnmopi  32683  stle0i  32774  stlesi  32776  stm1i  32778  csmdsymi  32869  cvmd  32871  atcveq0  32883  atcv1  32915  atord  32923  atcvat2  32924  chirred  32930  mdsym  32947  mddmdin0i  32966  cdj1i  32968  fmptcof2  33184  fnpreimac  33197  isoun  33228  fcobijfs  33246  fcobijfs2  33247  lt2addrd  33275  xlt2addrd  33284  xrge0infss  33285  infxrge0glb  33290  xrofsup  33292  fz1nnct  33326  toslublem  33466  tosglblem  33468  ismntd  33478  mgccole1  33484  mgccole2  33485  mgcmnt1  33486  mgcmnt2  33487  dfmgc2lem  33489  dfmgc2  33490  psgnfzto1stlem  33594  fzto1st  33597  psgnfzto1st  33599  trsp2cyc  33617  xrnarchi  33678  archirng  33682  archiexdiv  33684  archiabl  33692  isarchiofld  33693  elrgspnlem1  33736  elrgspnlem2  33737  elrgspnlem3  33738  elrgspnlem4  33739  elrgspn  33740  elrgspnsubrunlem1  33741  elrgspnsubrunlem2  33742  elrgspnsubrun  33743  linds2eq  33869  elrspunidl  33911  elrspunsn  33912  isrprm  33982  evl1deg1  34041  evl1deg2  34042  evl1deg3  34043  0mplrim  34079  selvply1rhmlema  34083  selvply1rhmlemb  34084  selvply1rhmlem1  34085  selvply1rhmlem2  34086  selvply1rhmlem4  34088  selvply1rhm0  34091  extvfvvcl  34100  extvfvcl  34101  mplmulmvr  34104  evlextv  34107  mplvrpmlem  34108  mplvrpmfgalem  34109  mplvrpmga  34110  mplvrpmmhm  34111  mplvrpmrhm  34112  psrmonmul  34115  psrmonprod  34117  esplyfval0  34129  esplylem  34131  esplyfv1  34134  esplyfval3  34137  esplyfvaln  34139  esplyind  34140  ply1degltdimlem  34187  lbsdiflsp0  34191  fedgmullem1  34194  fedgmullem2  34195  fedgmul  34196  fldextrspunlsplem  34238  fldextrspunlsp  34239  smatrcl  34361  smatlem  34362  madjusmdetlem2  34393  madjusmdet  34396  cmpcref  34415  ldlfcntref  34419  dispcmp  34424  zarcmplem  34446  ordtrest2NEWlem  34487  ordtconnlem1  34489  xrge0iifiso  34500  rge0scvg  34514  gsumesum  34624  esumfsup  34635  esumpinfval  34638  esumpcvgval  34643  esumcvg  34651  sigaclcu  34682  sigaclci  34697  unelsiga  34699  unelldsys  34724  sigapildsys  34728  ldgenpisyslem1  34729  fiunelros  34740  measvun  34775  voliune  34795  volfiniune  34796  oms0  34863  omssubaddlem  34865  omssubadd  34866  carsgsigalem  34881  carsgclctunlem2  34885  carsgclctun  34887  pmeasmono  34890  pmeasadd  34891  orvcval2  35025  dstfrvel  35040  ballotlemfc0  35059  ballotlemfcc  35060  ballotlemsv  35076  ballotlemsf1o  35080  breprexp  35196  tgoldbachgt  35226  bnj23  35283  bnj1185  35357  bnj1152  35562  bnj1418  35604  fnrelpredd  35650  kardval2  35746  elkarden  35748  kardeng  35750  kardnnfi  35762  rankkardu  35764  dfdm5  36459  dfrn5  36460  wzel  36508  wsuclem  36509  brpprod  36569  brsset  36573  brbigcup  36582  dffix2  36589  elfuns  36599  brimageg  36611  brdomaing  36619  brrangeg  36620  brimg  36621  brapply  36622  lemsuccf  36625  funpartlem  36628  brrestrict  36635  dfrecs2  36636  dfrdg4  36637  brofs  36692  btwncomim  36700  btwnintr  36706  btwnexch3  36707  btwnexch2  36710  brifs  36730  brcolinear2  36745  colineardim1  36748  brfs  36766  btwnconn1  36788  segcon2  36792  seglerflx  36799  seglemin  36800  btwnsegle  36804  colinbtwnle  36805  broutsideof2  36809  fvray  36828  lineunray  36834  lineelsb2  36835  linerflx1  36836  trer  37026  elicc3  37027  finminlem  37028  nn0prpwlem  37032  nn0prpw  37033  fnessref  37067  refssfne  37068  weiunlem  37173  weiunfrlem  37174  weiunfr  37177  weiunse  37178  unblimceq0lem  37294  unblimceq0  37295  unbdqndv2  37299  knoppndvlem21  37320  taupilemrplb  38161  dfgcd3  38165  icorempo  38194  icoreval  38196  iooelexlt  38205  relowlssretop  38206  domalom  38247  ctbssinf  38249  pibt2  38260  phpreu  38447  fin2solem  38449  fin2so  38450  ltflcei  38451  ptrecube  38458  poimirlem1  38459  poimirlem2  38460  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem9  38467  poimirlem12  38470  poimirlem22  38480  poimirlem23  38481  poimirlem24  38482  poimirlem26  38484  poimirlem27  38485  poimirlem32  38490  heicant  38493  mblfinlem1  38495  mblfinlem2  38496  itg2addnclem  38509  itg2addnclem3  38511  itg2addnc  38512  itg2gt0cn  38513  ibladdnclem  38514  iblmulc2nc  38523  itgabsnc  38527  ftc1anclem5  38535  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  indexdom  38588  filbcmb  38594  fdc  38599  prdsbnd  38647  heiborlem3  38667  rrnequiv  38689  rngoueqz  38794  eqbrtr  39090  elrnressn  39132  inxprnres  39150  presucmap  39347  eqvreltr  39543  prtlem10  39842  lsatcveq0  40009  lsatcv1  40025  oposlem  40159  opnlen0  40165  lub0N  40166  glb0N  40170  omllaw  40220  cmtbr4N  40232  cvrval  40246  cvrnbtwn  40248  cvrnbtwn2  40252  cvrnbtwn3  40253  cvrcon3b  40254  cvrnbtwn4  40256  atcvreq0  40291  atnle  40294  atlatmstc  40296  cvlexch1  40305  glbconN  40354  hlsuprexch  40358  exatleN  40381  cvratlem  40398  atcvrj0  40405  atcvrj2b  40409  atlelt  40415  cvrat4  40420  3dim1lem5  40443  3dim2  40445  3dim3  40446  ps-2  40455  llni  40485  llnn0  40493  llnle  40495  lplni  40509  lplni2  40514  lplnle  40517  lplnn0N  40524  llncvrlpln  40535  2llnjN  40544  lvoli  40552  lvoli3  40554  lvoli2  40558  lvoln0N  40568  4at  40590  lplncvrlvol  40593  2lplnj  40597  dalemcea  40637  dalem3  40641  psubspi  40724  linepsubN  40729  elpmap  40735  pmapsub  40745  lnatexN  40756  cdlema1N  40768  cdlemb  40771  elpadd  40776  paddvaln0N  40778  paddasslem5  40801  llnexchb2lem  40845  llnexch2N  40847  islhp  40973  lhpat3  41023  4atexlemex2  41048  4atex  41053  4atex2-0aOLDN  41055  4atex2-0cOLDN  41057  lautle  41061  lautcvr  41069  lauteq  41072  ldilval  41090  ltrnu  41098  trlval2  41140  trlne  41162  cdleme0ex1N  41200  cdleme0nex  41267  cdleme18d  41272  cdlemednuN  41277  cdleme25b  41331  cdleme25cv  41335  cdleme27b  41345  cdleme29b  41352  cdleme31sn  41357  cdleme31fv  41367  cdleme31fv2  41370  cdlemefrs29bpre0  41373  cdlemefr29bpre0N  41383  cdlemefr29clN  41384  cdlemefr32fvaN  41386  cdlemefr32fva1  41387  cdlemefs29pre00N  41389  cdlemefs32sn1aw  41391  cdlemefs29bpre0N  41393  cdlemefs29bpre1N  41394  cdlemefs29cpre1N  41395  cdlemefs29clN  41396  cdlemefs32fvaN  41399  cdlemefs32fva1  41400  cdleme41sn3a  41410  cdleme32fva  41414  cdleme32e  41422  cdleme35f  41431  cdleme40v  41446  cdleme42b  41455  trlord  41546  cdlemg1cex  41565  diaval  42009  diaeldm  42013  diaelrnN  42022  cdlemm10N  42095  dibglbN  42143  dicval  42153  dicfnN  42160  dicvalrelN  42162  dihval  42209  dihlsscpre  42211  dihglblem3N  42272  dihmeetlem2N  42276  djhcvat42  42392  lcmineqlem4  43002  aks4d1p4  43049  aks4d1p5  43050  aks4d1p7  43053  aks4d1p8d2  43055  aks4d1p8  43057  hashnexinjle  43099  sticksstones1  43116  sticksstones2  43117  sticksstones10  43125  sticksstones12a  43127  aks6d1c7lem4  43153  aks6d1c7  43154  grpods  43164  unitscyglem2  43166  unitscyglem3  43167  unitscyglem4  43168  qsalrel  43212  supinf  43213  dvdsexpnn0  43313  redvmptabs  43339  sn-nnne0  43452  sn-sup2  43483  fimgmcyclem  43519  flt4lem2  43597  flt4lem7  43609  lzenom  43719  fphpdo  43762  irrapxlem4  43770  pellexlem6  43779  infmrgelbi  43823  pellfundre  43826  pellfundlb  43829  monotoddzz  43888  zindbi  43891  jm2.27  43953  rmydioph  43959  rpnnen3lem  43976  fnwe2lem2  43996  aomclem8  44006  hbtlem5  44073  hbt  44075  sdomne0  44357  sdomne0d  44358  ensucne0  44473  sucomisnotcard  44488  en2pr  44491  pr2cv  44492  refimssco  44551  rfovfvfvd  44947  rfovcnvf1od  44948  fsovrfovd  44953  nzss  45245  relprel  45878  permaxinf2lem  45939  wessf1ornlem  46121  axccdom  46156  dmrelrnrel  46160  axccd  46162  rnmptlb  46176  rnmptbdd  46178  rnmptbd2  46182  rnmptbdlem  46188  rnmptbd  46189  dstregt0  46219  suplesup  46273  supxrunb3  46332  supxrleubrnmpt  46338  rexabslelem  46350  rexabsle  46351  suprleubrnmpt  46354  infrnmptle  46355  infxrunb3rnmpt  46360  infxrpnf  46378  supminfxr  46396  infrpgernmpt  46397  xrpnf  46417  limsupre  46573  limsupref  46617  limsupbnd1f  46618  limsuppnfd  46634  climinf2  46639  limsuppnf  46643  climinfmpt  46647  climinf3  46648  limsupmnflem  46652  limsupmnf  46653  limsupre2  46657  limsupmnfuzlem  46658  limsupre2mpt  46662  limsupre3lem  46664  limsupre3  46665  limsupre3mpt  46666  limsupre3uzlem  46667  limsupre3uz  46668  limsupreuz  46669  limsupreuzmpt  46671  liminfval2  46700  liminfreuzlem  46734  liminfreuz  46735  xlimpnfxnegmnf  46746  cnrefiisplem  46761  xlimpnfv  46770  xlimpnf  46774  xlimpnfmpt  46776  dfxlim2  46780  icccncfext  46819  cncficcgt0  46820  ioodvbdlimc1lem2  46864  ioodvbdlimc2lem  46866  stoweidlem5  46937  stoweidlem20  46952  stoweidlem26  46958  stoweidlem28  46960  stoweidlem29  46961  stoweidlem34  46966  wallispilem3  46999  stirlinglem13  47018  fourierdlem41  47080  fourierdlem42  47081  fourierdlem51  47089  fourierdlem54  47092  salunicl  47248  saluncl  47249  salexct  47266  salexct2  47271  salexct3  47274  salgencntex  47275  salgensscntex  47276  sge0pnffigt  47328  meadjuni  47389  omeunile  47437  ovnlerp  47494  hoidifhspval  47540  ovolval5lem2  47585  salpreimagelt  47639  pimincfltioo  47650  salpreimagtge  47657  salpreimagtlt  47662  incsmf  47674  issmfgt  47688  smfpreimagt  47694  decsmf  47699  issmfge  47702  smfpimgtxr  47712  smfpreimage  47714  smfinflem  47749  smfinf  47750  finfdm  47778  funressnfv  48035  funressnvmo  48037  funressnmo  48038  dfdfat2  48120  tz6.12-afv  48165  funressndmafv2rn  48215  tz6.12-afv2  48232  dfatcolem  48247  dfatco  48248  zplusmodne  48341  m1modne  48346  minusmod5ne  48347  submodneaddmod  48349  modmknepk  48360  iccpartigtl  48427  iccpartgt  48431  icceuelpartlem  48439  iccpartnel  48442  sprsymrelfolem2  48497  nprmmul2  48532  goldbachthlem2  48553  odz2prm2pw  48570  fmtnoprmfac1  48572  fmtnoprmfac2  48574  fmtnofac2  48576  fmtno4prmfac  48579  fmtno4prm  48582  prmdvdsfmtnof1lem1  48591  31prm  48604  nprmdvdsfacm1  48631  perfectALTVlem2  48742  nnsum3primes4  48808  nnsum3primesprm  48810  nnsum3primesgbe  48812  nnsum3primesle9  48814  nnsum4primeseven  48820  nnsum4primesevenALTV  48821  wtgoldbnnsum4prm  48822  bgoldbnnsum3prm  48824  bgoldbtbndlem4  48828  bgoldbtbnd  48829  tgblthelfgott  48835  tgoldbach  48837  assintop  49228  isassintop  49229  assintopcllaw  49231  ztprmneprm  49381  ply1mulgsumlem1  49420  ply1mulgsumlem2  49421  lco0  49461  lcoel0  49462  lincsumcl  49465  lincscmcl  49466  lcoss  49470  linindslinci  49482  lindslinindsimp1  49491  linds0  49499  el0ldep  49500  lindsrng01  49502  ldepspr  49507  islindeps2  49517  isldepslvec2  49519  zlmodzxzldep  49538  ldepsnlinc  49542  elbigo2r  49587  xpco2  49889  tposres0  49907  lubsscl  49990  glbsscl  49991  lubprlem  49992  ipolub  50018  ipoglb  50021  catprslem  50040  infsubc2  50091  nelsubc3lem  50100  cnelsubclem  50633