Theorem breq1 5110

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  breq12  5112  breq1i  5114  breq1d  5117  nbrne2  5129  brab1  5157  pocl  5575  swopolem  5577  swopo  5578  po2ne  5583  solin  5594  sotrieq  5598  sotr2  5601  isso2i  5604  somo  5606  dffr2  5620  frc  5622  frirr  5635  fr2nr  5636  wereu2  5656  vtoclr  5722  frsn  5747  brcog  5850  brcogw  5852  brcnvg  5863  dfdmf  5884  eldmg  5886  dmun  5898  dm0rn0  5912  dfrnf  5938  dmcosseq  5966  dmcosseqOLD  5967  dfres2  6041  imasng  6084  cotrg  6109  cnvsym  6112  asymref2  6115  sotri2  6127  somin1  6131  rnco  6252  coi1  6263  predtrss  6324  frpomin  6342  dffun2  6547  dffun6f  6552  funmo  6553  fun11  6611  fveq2  6882  eliman0  6919  nfunsn  6921  dffv2  6977  fvopab5  7024  dff3  7096  f1ompt  7107  fmptco  7126  dff13  7254  foeqcnvco  7304  isorel  7330  soisores  7331  soisoi  7332  isocnv  7334  isotr  7340  isomin  7341  isoini  7342  isopolem  7349  isosolem  7351  f1oiso  7355  f1oiso2  7356  weniso  7360  eqfunresadj  7366  caovordig  7622  caovordg  7624  caovord3d  7627  caovord  7628  caovord3  7630  caofrss  7720  caoftrn  7722  fr3nr  7774  dfwe2  7776  f1oweALT  7972  frxp  8127  poxp  8129  fnse  8134  poxp2  8144  frxp2  8145  poxp3  8151  frxp3  8152  xpord3pred  8153  poseq  8159  brtpos2  8233  rntpos  8240  tpostpos  8247  frrlem12  8299  ertr  8715  ecopovsym  8822  ecopovtrn  8823  isfi  8984  en0  9027  en0ALT  9028  en1  9033  endisj  9065  xpcomco  9068  sbth  9098  2pwne  9134  disjenex  9136  ssenen  9152  findcard  9161  findcard2  9162  pssnn  9166  sbthfi  9196  nneneq  9203  php  9204  onomeneq  9211  sdom1  9223  1sdom2dom  9227  isinf  9238  fineqvlem  9239  en1eqsnbi  9249  findcard3  9256  frfi  9258  fiint  9299  mapfienlem1  9378  mapfienlem2  9379  mapfienlem3  9380  mapfien  9381  marypha1lem  9406  supmo  9425  eqsup  9429  supub  9432  suplub  9433  suppr  9445  supisolem  9447  supisoex  9448  infmin  9469  infmo  9470  fiinfg  9474  fiinf2g  9475  infpr  9478  ordtypecbv  9492  ordtypelem3  9495  ordtypelem6  9498  ordtypelem7  9499  ordtypelem9  9501  ordtypelem10  9502  hartogslem1  9517  hartogs  9519  wemaplem1  9521  wemaplem2  9522  wemapso2lem  9527  card2on  9529  card2inf  9530  elharval  9536  brwdom2  9548  wdomtr  9550  cantnfs  9648  cantnfp1lem2  9661  oemapso  9664  cantnflem1  9671  wemapwe  9679  ttrclss  9702  r111  9760  kardexOLD  9900  karden  9901  kardenOLD  9902  isnumi  9954  tskwe  9958  cardid2  9961  cardonle  9965  cardne  9973  iscard2  9984  infxpenlem  10019  fodomfi2  10066  wdomfil  10067  wdomnumr  10070  alephsuc2  10086  infenaleph  10097  iunfictbso  10120  infpss  10221  cff1  10263  cfslb2n  10273  sornom  10282  fin4i  10303  isfin6  10305  isfin7  10306  isfin1-3  10391  fin1a2lem9  10413  fin1a2lem11  10415  hsmexlem4  10434  axcc2lem  10441  axcc4dom  10446  domtriomlem  10447  numthcor  10499  zorn2lem2  10502  zorn2lem3  10503  zorn2lem7  10507  zorn2g  10508  axdclem  10524  axdc  10526  brdom7disj  10537  brdom6disj  10538  uniimadom  10555  ondomon  10574  alephval2  10584  alephreg  10594  pwcfsdom  10595  elgch  10634  gchi  10636  fpwwe2lem11  10653  fpwwe2lem12  10654  winainflem  10705  winalim2  10708  tsken  10766  0tsk  10767  inar1  10787  tskord  10792  tskuni  10795  grudomon  10829  pinq  10939  nqereu  10941  enqeq  10946  ltbtwnnq  10990  ltrnq  10991  prcdnq  11005  prnmax  11007  genpnmax  11019  nqpr  11026  1idpr  11041  reclem2pr  11060  reclem3pr  11061  reclem4pr  11062  recexpr  11063  supexpr  11066  ltsosr  11106  1ne0sr  11108  ltasr  11112  supsrlem  11123  axpre-lttri  11177  axpre-lttrn  11178  axpre-ltadd  11179  axpre-sup  11181  lelttr  11327  dedekind  11400  dedekindle  11401  ltordlem  11766  lt0ne0d  11806  fimaxre3  12188  fiminre2  12190  lbreu  12192  lble  12194  sup2  12198  infm3  12201  suprleub  12208  supaddc  12209  supadd  12210  supmul1  12211  supmullem1  12212  supmul  12214  nnne0  12297  nnsub  12307  nominpos  12508  nnunb  12527  arch  12528  nn0sub  12581  nn0n0n1ge2b  12600  nn0lt10b  12686  zextle  12697  peano5uzti  12714  fzind  12722  btwnz  12727  uzval  12892  uzwo  12963  nnwof  12966  ublbneg  12985  lbzbi  12988  zsupss  12989  uzsupss  12992  uzwo3  12995  zmax  12997  rebtwnz  12999  rpnnen1lem3  13031  xrltnsym  13190  xrlttri  13192  xrlttr  13193  xrlelttr  13209  nltpnft  13218  xrmaxlt  13235  xrmaxle  13237  qbtwnre  13253  qbtwnxr  13254  xltnegi  13270  xnn0lenn0nn0  13299  xsubge0  13315  xlesubadd  13317  xmullem2  13319  xlemul1a  13342  xrinfmexpnf  13360  xrsupsslem  13361  xrinfmsslem  13362  xrub  13366  supxrunb1  13373  supxrunb2  13374  reltre  13395  rpltrp  13396  reltxrnmnf  13397  ixxval  13408  elixx1  13409  elioo2  13441  iccid  13445  icc0  13448  fzval  13565  elfz1  13568  elfznelfzo  13831  elfznelfzob  13832  flval  13857  fllelt  13860  flflp1  13870  flval2  13877  flval3  13878  flbi  13879  dfceil2  13902  ceilval2  13903  fleqceilz  13917  modid2  13961  addmodlteq  14012  fsequb2  14042  ssnn0fi  14051  seqf1olem2  14108  sqlecan  14275  faclbnd4lem1  14359  hashsnle1  14484  pr2pwpr  14546  hash3tpde  14560  rtrclreclem3  15135  relexpindlem  15138  sgnval  15163  sgnmulsgn  15184  01sqrexlem6  15336  01sqrex  15338  abslt  15404  absle  15405  rexanre  15436  rexico  15443  limsupgle  15566  limsupgre  15570  limsupbnd2  15572  rlim2lt  15586  rlim3  15587  ello12r  15606  ello1d  15612  elo12r  15617  rlimconst  15633  climshft  15665  rlimcn3  15679  o1rlimmul  15708  lo1le  15741  climsup  15759  caucvgrlem  15762  isumless  15936  divrcnv  15943  cvgrat  15974  rpnnen2lem10  16315  ruclem1  16323  ruclem2  16324  ruclem11  16332  ruclem12  16333  sqrt2irr  16341  absdvdsb  16368  dvdsle  16404  dvdsabseq  16407  dvdsdivcl  16410  dvdsext  16415  divalglem8  16494  divalglem9  16495  divalglem10  16496  divalgmod  16500  ndvdssub  16503  sadcaddlem  16551  gcdcllem1  16593  gcdcllem2  16594  gcdcllem3  16595  dfgcd2  16640  gcdzeq  16646  dvdssq  16661  nn0seqcvgd  16664  algcvgblem  16671  lcmval  16686  lcmdvds  16702  lcmgcdeq  16706  lcmfpr  16721  lcmf  16727  lcmftp  16730  lcmfunsnlem1  16731  lcmfunsnlem2lem1  16732  lcmfunsnlem2lem2  16733  lcmfdvdsb  16737  coprmgcdb  16743  coprmdvds1  16746  1nprm  16773  1idssfct  16774  isprm2lem  16775  isprm2  16776  dvdsprime  16781  nprm  16782  3prm  16788  dvdsprm  16798  exprmfct  16799  isprm5  16802  maxprmfct  16804  coprm  16806  prmdvdsncoprmbd  16822  ncoprmlnprm  16823  eulerthlem2  16877  phisum  16886  odzval  16887  pythagtriplem4  16915  pc2dvds  16975  pcprmpw2  16978  pcprmpw  16979  dvdsprmpweqle  16982  oddprmdvds  16999  prmpwdvds  17000  pockthg  17002  unbenlem  17004  prmreclem4  17015  prmreclem5  17016  prmreclem6  17017  1arith  17023  vdwlem6  17082  vdwlem11  17087  vdwlem13  17089  ramtlecl  17096  ramub  17109  rami  17111  ramubcl  17114  0ram  17116  ram0  17118  prmdvdsprmop  17139  prmolefac  17142  prmodvdslcmf  17143  prmgaplem2  17146  prmgaplcmlem1  17147  prmgaplcmlem2  17148  prmgaplem3  17149  prmgaplem4  17150  prmgaplem5  17151  prmgaplem6  17152  prmgapprmolem  17157  prmlem0  17201  prmlem1a  17202  imasaddfnlem  17618  imasvscafn  17627  imasleval  17631  prslem  18389  drsdir  18394  drsdirfi  18397  isdrs2  18398  posi  18409  posasymb  18411  pospropd  18417  pltval3  18429  plelttr  18434  pospo  18435  lubprop  18448  luble  18449  lublecllem  18450  glbprop  18461  joinval2lem  18470  joinlem  18473  meetlem  18487  meetle  18490  poslubmo  18501  posglbmo  18502  poslubd  18503  tleile  18511  latnlej  18548  isglbd  18601  lubub  18603  lubun  18607  clatleglb  18610  tsrlin  18677  letsr  18685  dirge  18695  pmtrval  19579  pmtrrn  19585  pmtrfrn  19586  pmtrrn2  19588  pmtrsn  19647  mndodcongi  19671  odeq  19678  odmulgeq  19685  gexnnod  19716  sylow1lem1  19726  pgpssslw  19742  sylow2a  19747  efgredeu  19880  efgred2  19881  gexex  19981  frgpnabllem2  20002  cyggenod  20012  dprdval  20133  dprdw  20140  dprdwd  20141  ablfacrplem  20195  ablfac1c  20201  ablfac1eu  20203  ablfaclem3  20217  omndadd  20256  abvtrivd  20999  zringlpir  21681  prmirredlem  21686  znleval  21768  frlmelbas  21970  ellspd  22016  islindf4  22052  psrbagconcl  22143  psrbagleadd1  22144  gsumbagdiaglem  22147  rhmpsrlem2  22157  psrlidm  22177  psrridm  22178  psrass1  22179  psrcom  22183  mplelbas  22206  mplmonmul  22253  ltbwe  22261  mhpmulcl  22378  psdmul  22395  coe1fsupp  22440  coe1ae0  22442  coe1mul2  22496  coe1tmmul  22504  pmatcoe1fsupp  22927  chfacffsupp  23082  chfacfscmulfsupp  23085  chfacfscmulgsum  23086  chfacfpmmulfsupp  23089  chfacfpmmulgsum  23090  ordtbas2  23417  ordtopn2  23421  ordtrest2lem  23429  pnfnei  23446  ordtt1  23605  ordthauslem  23609  2ndci  23674  2ndcsb  23675  2ndcredom  23676  2ndc1stc  23677  1stcrest  23679  2ndcctbss  23682  2ndcdisj  23683  2ndcsep  23686  lly1stc  23723  tx1stc  23877  ordthmeolem  24028  ufildom1  24153  xmetrtri2  24583  prdsxmetlem  24595  ssblex  24655  prdsbl  24718  comet  24740  stdbdxmet  24742  stdbdmopn  24745  met1stc  24748  dscmet  24799  metdstri  25079  metdscn  25084  xrhmeo  25175  bndth  25187  evth  25188  lebnumlem3  25192  pcovalg  25241  pco1  25244  pcocn  25246  pcopt  25251  pcopt2  25252  pcoass  25253  nmoleub3  25348  bcthlem5  25557  rrxfsupp  25631  minveclem4c  25654  minveclem2  25655  minveclem3b  25657  minveclem4  25661  minveclem6  25663  pmltpclem1  25677  pmltpc  25679  ovollb2lem  25717  ovolctb  25719  ovolunlem1  25726  ovoliunlem1  25731  ovoliunlem2  25732  ovoliun2  25735  ovolshftlem1  25738  ovolscalem1  25742  ovolicc1  25745  ovolicc2lem3  25748  voliunlem2  25780  voliunlem3  25781  ioombl1lem4  25790  uniioovol  25808  uniioombllem2  25812  uniioombllem3  25814  uniioombllem6  25817  volsup2  25834  ismbfd  25868  mbfsup  25893  mbflimsup  25895  itg1climres  25943  mbfi1fseqlem4  25947  itg2lr  25959  itg2leub  25963  itg2seq  25971  itg2monolem1  25979  itg2monolem3  25981  itg2mono  25982  itg2i1fseq2  25985  itg2gt0  25989  itg2cnlem1  25990  itg2cnlem2  25991  itg2cn  25992  iblss  26034  itgless  26046  ibladdlem  26049  iblabsr  26059  iblmulc2  26060  itgabs  26064  bddiblnc  26071  ditgeq1  26077  dvferm2lem  26215  rolle  26219  dvlip2  26224  c1liplem1  26225  c1lip1  26226  dvfsumlem2  26256  dvfsumlem4  26258  mdegleb  26291  degltlem1  26299  plyco0  26419  plyeq0lem  26437  coeeq2  26469  dgrle  26470  dgradd2  26495  plydiveu  26529  aareccl  26559  aalioulem2  26566  aaliou3lem7  26582  psercnlem1  26658  pilem2  26685  pilem3  26686  logltb  26835  divlogrlim  26870  logcnlem3  26879  cxpaddlelem  26986  rlimcnp  27200  cxplim  27206  cxploglim  27212  scvxcvx  27220  ftalem1  27307  ftalem2  27308  isppw2  27349  vmappw  27350  sgmnncl  27381  sqff1o  27416  fsumdvdsdiaglem  27417  dvdsppwf1o  27420  dvdsflsumcom  27422  musum  27425  muinv  27427  mpodvdsmulf1o  27428  dvdsmulf1o  27430  vmalelog  27439  vmasum  27450  logfac2  27451  perfectlem2  27464  bcmono  27511  bpos1lem  27516  bposlem9  27526  lgsmod  27557  lgsne0  27569  gausslemma2dlem4  27603  2sqlem6  27657  2sqlem8  27660  2sqlem10  27662  2sqreulem1  27680  2sqreunnlem1  27683  chtppilim  27709  rpvmasumlem  27721  dchrisumlema  27722  dchrisumlem2  27724  dchrvmasumlem1  27729  dchrvmasumiflem1  27735  dchrisum0flblem1  27742  dchrisum0flblem2  27743  dchrisum0  27754  rplogsum  27761  logsqvma  27776  pntpbnd1  27820  pntpbnd2  27821  pntibndlem3  27826  pntlemj  27837  pntlemi  27838  pntlem3  27843  pnt3  27846  ostth3  27872  nodense  27926  noresle  27931  nosupprefixmo  27934  noinfprefixmo  27935  nosupcbv  27936  nosupdm  27938  nosupbnd1lem1  27942  nosupbnd1lem4  27945  nosupbnd1  27948  nosupbnd2lem1  27949  nosupbnd2  27950  noinfcbv  27951  noinfdm  27953  noinffv  27955  noinfres  27956  noinfbnd1lem3  27959  noinfbnd1lem4  27960  noinfbnd1lem5  27961  noinfbnd1  27963  noetalem2  27976  nocvxminlem  28017  sltssnb  28032  sltssepc  28034  conway  28042  cutsval  28043  etaslts  28056  lesrec  28062  eqcuts3  28067  bday1  28077  cuteq1  28080  madeval2  28096  rightval  28113  elleft  28114  sltsright  28124  made0  28126  madecut  28146  left1s  28158  madebdaylemlrcut  28162  ltslpss  28171  cofslts  28181  coinitslts  28182  cofcutr  28187  cofcutrtime  28190  cofss  28193  coiniss  28194  cutmax  28197  cutmin  28198  cutminmax  28199  addsproplem1  28232  addsprop  28239  leadds1  28252  addsuniflem  28264  negsproplem1  28291  negsprop  28298  negsid  28304  negsunif  28318  mulsproplemcbv  28378  mulsproplem1  28379  mulsproplem9  28387  mulsprop  28393  sltmuls1  28410  sltmuls2  28411  mulsuniflem  28412  precsexlem11  28480  abslts  28512  oncutlt  28527  oniso  28534  bdayons  28539  addonbday  28542  n0fincut  28618  onsfi  28619  n0subs  28626  bdayn0p1  28632  eucliddivs  28639  zcuts  28670  twocut  28686  halfcut  28721  addhalfcut  28722  bdaypw2n0bndlem  28726  bdayfinbndcbv  28729  bdayfinbndlem1  28730  bdayfinbndlem2  28731  z12bdaylem1  28733  elreno  28754  elreno2  28758  tgjustc1  28814  tgjustc2  28815  iscgrglt  28854  tgcgr4  28871  hlcgreu  28961  elplng  29135  plngcplem  29140  lmif  29167  islmib  29169  trgcopyeu  29190  iscgrad  29195  inaghl  29241  axlowdim2  29403  axlowdim  29404  axcontlem2  29408  axcontlem3  29409  axcontlem4  29410  axcontlem7  29413  axcontlem9  29415  axcontlem10  29416  axcontlem11  29417  axcontlem12  29418  ebtwntg  29425  umgrupgr  29546  nbusgrvtxm1  29825  crctcshwlkn0lem2  30265  crctcshwlkn0lem3  30266  crctcsh  30278  wlkswwlksf1o  30333  clwlkclwwlklem2fv1  30451  clwlkclwwlkf  30464  0clwlkv  30587  loop1cycl  30609  umgr2cycl  30612  acycgrcycl  30618  eupth2  30705  numclwwlk5  30854  nmoubi  31239  minvecolem2  31342  minvecolem3  31343  minvecolem4c  31346  minvecolem4  31347  minvecolem5  31348  minvecolem6  31349  htthlem  31384  chlimi  31701  chcompl  31709  hsn0elch  31715  cmbr3  32075  cmcm  32081  cmcm3  32082  lecm  32084  nmopub  32375  nmfnleub  32392  nmopun  32481  nmcexi  32493  cnlnadjlem7  32540  pjnmopi  32615  stle0i  32706  stlesi  32708  stm1i  32710  csmdsymi  32801  cvmd  32803  atcveq0  32815  atcv1  32847  atord  32855  atcvat2  32856  chirred  32862  mdsym  32879  mddmdin0i  32898  cdj1i  32900  fmptcof2  33117  fnpreimac  33130  isoun  33161  fcobijfs  33179  fcobijfs2  33180  lt2addrd  33208  xlt2addrd  33217  xrge0infss  33218  infxrge0glb  33223  xrofsup  33225  fz1nnct  33259  toslublem  33399  tosglblem  33401  ismntd  33411  mgccole1  33417  mgccole2  33418  mgcmnt1  33419  mgcmnt2  33420  dfmgc2lem  33422  dfmgc2  33423  psgnfzto1stlem  33527  fzto1st  33530  psgnfzto1st  33532  trsp2cyc  33550  xrnarchi  33611  archirng  33615  archiexdiv  33617  archiabl  33625  isarchiofld  33626  elrgspnlem1  33669  elrgspnlem2  33670  elrgspnlem3  33671  elrgspnlem4  33672  elrgspn  33673  elrgspnsubrunlem1  33674  elrgspnsubrunlem2  33675  elrgspnsubrun  33676  linds2eq  33801  elrspunidl  33843  elrspunsn  33844  isrprm  33914  evl1deg1  33973  evl1deg2  33974  evl1deg3  33975  0mplrim  34011  selvply1rhmlema  34015  selvply1rhmlemb  34016  selvply1rhmlem1  34017  selvply1rhmlem2  34018  selvply1rhmlem4  34020  selvply1rhm0  34023  extvfvvcl  34032  extvfvcl  34033  mplmulmvr  34036  evlextv  34039  mplvrpmlem  34040  mplvrpmfgalem  34041  mplvrpmga  34042  mplvrpmmhm  34043  mplvrpmrhm  34044  psrmonmul  34047  psrmonprod  34049  esplyfval0  34061  esplylem  34063  esplyfv1  34066  esplyfval3  34069  esplyfvaln  34071  esplyind  34072  ply1degltdimlem  34119  lbsdiflsp0  34123  fedgmullem1  34126  fedgmullem2  34127  fedgmul  34128  fldextrspunlsplem  34170  fldextrspunlsp  34171  smatrcl  34293  smatlem  34294  madjusmdetlem2  34325  madjusmdet  34328  cmpcref  34347  ldlfcntref  34351  dispcmp  34356  zarcmplem  34378  ordtrest2NEWlem  34419  ordtconnlem1  34421  xrge0iifiso  34432  rge0scvg  34446  gsumesum  34556  esumfsup  34567  esumpinfval  34570  esumpcvgval  34575  esumcvg  34583  sigaclcu  34614  sigaclci  34629  unelsiga  34631  unelldsys  34656  sigapildsys  34660  ldgenpisyslem1  34661  fiunelros  34672  measvun  34707  voliune  34727  volfiniune  34728  oms0  34795  omssubaddlem  34797  omssubadd  34798  carsgsigalem  34813  carsgclctunlem2  34817  carsgclctun  34819  pmeasmono  34822  pmeasadd  34823  orvcval2  34957  dstfrvel  34972  ballotlemfc0  34991  ballotlemfcc  34992  ballotlemsv  35008  ballotlemsf1o  35012  breprexp  35128  tgoldbachgt  35158  bnj23  35215  bnj1185  35289  bnj1152  35494  bnj1418  35536  fnrelpredd  35583  kardval2  35666  elkarden  35668  kardeng  35670  kardnnfi  35682  rankkardu  35684  dfdm5  36339  dfrn5  36340  wzel  36388  wsuclem  36389  brpprod  36449  brsset  36453  brbigcup  36462  dffix2  36469  elfuns  36479  brimageg  36491  brdomaing  36499  brrangeg  36500  brimg  36501  brapply  36502  lemsuccf  36505  funpartlem  36508  brrestrict  36515  dfrecs2  36516  dfrdg4  36517  brofs  36572  btwncomim  36580  btwnintr  36586  btwnexch3  36587  btwnexch2  36590  brifs  36610  brcolinear2  36625  colineardim1  36628  brfs  36646  btwnconn1  36668  segcon2  36672  seglerflx  36679  seglemin  36680  btwnsegle  36684  colinbtwnle  36685  broutsideof2  36689  fvray  36708  lineunray  36714  lineelsb2  36715  linerflx1  36716  trer  36922  elicc3  36923  finminlem  36924  nn0prpwlem  36928  nn0prpw  36929  fnessref  36963  refssfne  36964  weiunlem  37069  weiunfrlem  37070  weiunfr  37073  weiunse  37074  unblimceq0lem  37190  unblimceq0  37191  unbdqndv2  37195  knoppndvlem21  37216  taupilemrplb  38059  dfgcd3  38063  icorempo  38092  icoreval  38094  iooelexlt  38103  relowlssretop  38104  domalom  38145  ctbssinf  38147  pibt2  38158  phpreu  38345  fin2solem  38347  fin2so  38348  ltflcei  38349  ptrecube  38356  poimirlem1  38357  poimirlem2  38358  poimirlem5  38361  poimirlem6  38362  poimirlem7  38363  poimirlem9  38365  poimirlem12  38368  poimirlem22  38378  poimirlem23  38379  poimirlem24  38380  poimirlem26  38382  poimirlem27  38383  poimirlem32  38388  heicant  38391  mblfinlem1  38393  mblfinlem2  38394  itg2addnclem  38407  itg2addnclem3  38409  itg2addnc  38410  itg2gt0cn  38411  ibladdnclem  38412  iblmulc2nc  38421  itgabsnc  38425  ftc1anclem5  38433  ftc1anclem7  38435  ftc1anclem8  38436  ftc1anc  38437  indexdom  38471  filbcmb  38477  fdc  38482  prdsbnd  38530  heiborlem3  38550  rrnequiv  38572  rngoueqz  38677  eqbrtr  38973  elrnressn  39015  inxprnres  39033  presucmap  39230  eqvreltr  39426  prtlem10  39725  lsatcveq0  39892  lsatcv1  39908  oposlem  40042  opnlen0  40048  lub0N  40049  glb0N  40053  omllaw  40103  cmtbr4N  40115  cvrval  40129  cvrnbtwn  40131  cvrnbtwn2  40135  cvrnbtwn3  40136  cvrcon3b  40137  cvrnbtwn4  40139  atcvreq0  40174  atnle  40177  atlatmstc  40179  cvlexch1  40188  glbconN  40237  hlsuprexch  40241  exatleN  40264  cvratlem  40281  atcvrj0  40288  atcvrj2b  40292  atlelt  40298  cvrat4  40303  3dim1lem5  40326  3dim2  40328  3dim3  40329  ps-2  40338  llni  40368  llnn0  40376  llnle  40378  lplni  40392  lplni2  40397  lplnle  40400  lplnn0N  40407  llncvrlpln  40418  2llnjN  40427  lvoli  40435  lvoli3  40437  lvoli2  40441  lvoln0N  40451  4at  40473  lplncvrlvol  40476  2lplnj  40480  dalemcea  40520  dalem3  40524  psubspi  40607  linepsubN  40612  elpmap  40618  pmapsub  40628  lnatexN  40639  cdlema1N  40651  cdlemb  40654  elpadd  40659  paddvaln0N  40661  paddasslem5  40684  llnexchb2lem  40728  llnexch2N  40730  islhp  40856  lhpat3  40906  4atexlemex2  40931  4atex  40936  4atex2-0aOLDN  40938  4atex2-0cOLDN  40940  lautle  40944  lautcvr  40952  lauteq  40955  ldilval  40973  ltrnu  40981  trlval2  41023  trlne  41045  cdleme0ex1N  41083  cdleme0nex  41150  cdleme18d  41155  cdlemednuN  41160  cdleme25b  41214  cdleme25cv  41218  cdleme27b  41228  cdleme29b  41235  cdleme31sn  41240  cdleme31fv  41250  cdleme31fv2  41253  cdlemefrs29bpre0  41256  cdlemefr29bpre0N  41266  cdlemefr29clN  41267  cdlemefr32fvaN  41269  cdlemefr32fva1  41270  cdlemefs29pre00N  41272  cdlemefs32sn1aw  41274  cdlemefs29bpre0N  41276  cdlemefs29bpre1N  41277  cdlemefs29cpre1N  41278  cdlemefs29clN  41279  cdlemefs32fvaN  41282  cdlemefs32fva1  41283  cdleme41sn3a  41293  cdleme32fva  41297  cdleme32e  41305  cdleme35f  41314  cdleme40v  41329  cdleme42b  41338  trlord  41429  cdlemg1cex  41448  diaval  41892  diaeldm  41896  diaelrnN  41905  cdlemm10N  41978  dibglbN  42026  dicval  42036  dicfnN  42043  dicvalrelN  42045  dihval  42092  dihlsscpre  42094  dihglblem3N  42155  dihmeetlem2N  42159  djhcvat42  42275  lcmineqlem4  42885  aks4d1p4  42932  aks4d1p5  42933  aks4d1p7  42936  aks4d1p8d2  42938  aks4d1p8  42940  hashnexinjle  42982  sticksstones1  42999  sticksstones2  43000  sticksstones10  43008  sticksstones12a  43010  aks6d1c7lem4  43036  aks6d1c7  43037  grpods  43047  unitscyglem2  43049  unitscyglem3  43050  unitscyglem4  43051  qsalrel  43095  supinf  43096  dvdsexpnn0  43196  redvmptabs  43222  sn-nnne0  43335  sn-sup2  43366  fimgmcyclem  43402  flt4lem2  43480  flt4lem7  43492  lzenom  43602  fphpdo  43645  irrapxlem4  43653  pellexlem6  43662  infmrgelbi  43706  pellfundre  43709  pellfundlb  43712  monotoddzz  43771  zindbi  43774  jm2.27  43836  rmydioph  43842  rpnnen3lem  43859  fnwe2lem2  43879  aomclem8  43889  hbtlem5  43956  hbt  43958  sdomne0  44240  sdomne0d  44241  ensucne0  44356  sucomisnotcard  44371  en2pr  44374  pr2cv  44375  refimssco  44434  rfovfvfvd  44830  rfovcnvf1od  44831  fsovrfovd  44836  nzss  45128  relprel  45761  permaxinf2lem  45822  wessf1ornlem  46004  axccdom  46039  dmrelrnrel  46043  axccd  46045  rnmptlb  46059  rnmptbdd  46061  rnmptbd2  46065  rnmptbdlem  46071  rnmptbd  46072  dstregt0  46102  suplesup  46156  supxrunb3  46215  supxrleubrnmpt  46221  rexabslelem  46233  rexabsle  46234  suprleubrnmpt  46237  infrnmptle  46238  infxrunb3rnmpt  46243  infxrpnf  46261  supminfxr  46279  infrpgernmpt  46280  xrpnf  46300  limsupre  46456  limsupref  46500  limsupbnd1f  46501  limsuppnfd  46517  climinf2  46522  limsuppnf  46526  climinfmpt  46530  climinf3  46531  limsupmnflem  46535  limsupmnf  46536  limsupre2  46540  limsupmnfuzlem  46541  limsupre2mpt  46545  limsupre3lem  46547  limsupre3  46548  limsupre3mpt  46549  limsupre3uzlem  46550  limsupre3uz  46551  limsupreuz  46552  limsupreuzmpt  46554  liminfval2  46583  liminfreuzlem  46617  liminfreuz  46618  xlimpnfxnegmnf  46629  cnrefiisplem  46644  xlimpnfv  46653  xlimpnf  46657  xlimpnfmpt  46659  dfxlim2  46663  icccncfext  46702  cncficcgt0  46703  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  stoweidlem5  46820  stoweidlem20  46835  stoweidlem26  46841  stoweidlem28  46843  stoweidlem29  46844  stoweidlem34  46849  wallispilem3  46882  stirlinglem13  46901  fourierdlem41  46963  fourierdlem42  46964  fourierdlem51  46972  fourierdlem54  46975  salunicl  47131  saluncl  47132  salexct  47149  salexct2  47154  salexct3  47157  salgencntex  47158  salgensscntex  47159  sge0pnffigt  47211  meadjuni  47272  omeunile  47320  ovnlerp  47377  hoidifhspval  47423  ovolval5lem2  47468  salpreimagelt  47522  pimincfltioo  47533  salpreimagtge  47540  salpreimagtlt  47545  incsmf  47557  issmfgt  47571  smfpreimagt  47577  decsmf  47582  issmfge  47585  smfpimgtxr  47595  smfpreimage  47597  smfinflem  47632  smfinf  47633  finfdm  47661  funressnfv  47918  funressnvmo  47920  funressnmo  47921  dfdfat2  48003  tz6.12-afv  48048  funressndmafv2rn  48098  tz6.12-afv2  48115  dfatcolem  48130  dfatco  48131  zplusmodne  48224  m1modne  48229  minusmod5ne  48230  submodneaddmod  48232  modmknepk  48243  iccpartigtl  48310  iccpartgt  48314  icceuelpartlem  48322  iccpartnel  48325  sprsymrelfolem2  48380  nprmmul2  48415  goldbachthlem2  48436  odz2prm2pw  48453  fmtnoprmfac1  48455  fmtnoprmfac2  48457  fmtnofac2  48459  fmtno4prmfac  48462  fmtno4prm  48465  prmdvdsfmtnof1lem1  48474  31prm  48487  nprmdvdsfacm1  48514  perfectALTVlem2  48625  nnsum3primes4  48691  nnsum3primesprm  48693  nnsum3primesgbe  48695  nnsum3primesle9  48697  nnsum4primeseven  48703  nnsum4primesevenALTV  48704  wtgoldbnnsum4prm  48705  bgoldbnnsum3prm  48707  bgoldbtbndlem4  48711  bgoldbtbnd  48712  tgblthelfgott  48718  tgoldbach  48720  assintop  49111  isassintop  49112  assintopcllaw  49114  ztprmneprm  49264  ply1mulgsumlem1  49303  ply1mulgsumlem2  49304  lco0  49344  lcoel0  49345  lincsumcl  49348  lincscmcl  49349  lcoss  49353  linindslinci  49365  lindslinindsimp1  49374  linds0  49382  el0ldep  49383  lindsrng01  49385  ldepspr  49390  islindeps2  49400  isldepslvec2  49402  zlmodzxzldep  49421  ldepsnlinc  49425  elbigo2r  49470  xpco2  49772  tposres0  49790  lubsscl  49873  glbsscl  49874  lubprlem  49875  ipolub  49901  ipoglb  49904  catprslem  49923  infsubc2  49974  nelsubc3lem  49983  cnelsubclem  50516  setrec2lem1  50606