Theorem breq1 5113

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ⟨cop 4598   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  breq12  5115  breq1i  5117  breq1d  5120  nbrne2  5130  brab1  5158  pocl  5557  swopolem  5559  swopo  5560  po2ne  5565  solin  5576  sotrieq  5580  sotr2  5583  isso2i  5586  somo  5588  dffr2  5602  frc  5604  frirr  5617  fr2nr  5618  wereu2  5638  vtoclr  5704  frsn  5729  brcog  5833  brcogw  5835  brcnvg  5846  dfdmf  5863  eldmg  5865  dfrnf  5917  dmcosseq  5943  dfres2  6015  imasng  6058  cotrg  6083  cnvsym  6088  asymref2  6093  sotri2  6105  somin1  6109  coi1  6238  predtrss  6298  frpomin  6316  dffun2  6524  dffun6f  6532  funmo  6534  funmoOLD  6535  fun11  6593  fveq2  6861  eliman0  6901  nfunsn  6903  dffv2  6959  fvopab5  7004  dff3  7075  f1ompt  7086  fmptco  7104  dff13  7232  foeqcnvco  7278  isorel  7304  soisores  7305  soisoi  7306  isocnv  7308  isotr  7314  isomin  7315  isoini  7316  isopolem  7323  isosolem  7325  f1oiso  7329  f1oiso2  7330  weniso  7332  eqfunresadj  7338  caovordig  7597  caovordg  7599  caovord3d  7602  caovord  7603  caovord3  7605  caofrss  7695  caoftrn  7697  fr3nr  7751  dfwe2  7753  f1oweALT  7954  frxp  8108  poxp  8110  fnse  8115  poxp2  8125  frxp2  8126  poxp3  8132  frxp3  8133  xpord3pred  8134  poseq  8140  brtpos2  8214  rntpos  8221  tpostpos  8228  frrlem12  8279  ertr  8689  ecopovsym  8795  ecopovtrn  8796  isfi  8950  en0  8992  en0ALT  8993  en1  8998  endisj  9032  xpcomco  9036  sbth  9067  2pwne  9103  disjenex  9105  ssenen  9121  findcard  9133  findcard2  9134  pssnn  9138  sbthfi  9169  nneneq  9176  php  9177  onomeneq  9184  sdom1  9196  sdom1OLD  9197  1sdom2dom  9201  isinf  9214  isinfOLD  9215  fineqvlem  9216  en1eqsnbi  9228  enp1iOLD  9232  findcard3  9236  findcard3OLD  9237  frfi  9239  fiint  9284  fiintOLD  9285  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  9626  cantnfp1lem2  9639  oemapso  9642  cantnflem1  9649  wemapwe  9657  ttrclss  9680  r111  9735  kardex  9854  karden  9855  isnumi  9906  tskwe  9910  cardid2  9913  cardonle  9917  cardne  9925  iscard2  9936  infxpenlem  9973  fodomfi2  10020  wdomfil  10021  wdomnumr  10024  alephsuc2  10040  infenaleph  10051  iunfictbso  10074  infpss  10176  cff1  10218  cfslb2n  10228  sornom  10237  fin4i  10258  isfin6  10260  isfin7  10261  isfin1-3  10346  fin1a2lem9  10368  fin1a2lem11  10370  hsmexlem4  10389  axcc2lem  10396  axcc4dom  10401  domtriomlem  10402  numthcor  10454  zorn2lem2  10457  zorn2lem3  10458  zorn2lem7  10462  zorn2g  10463  axdclem  10479  axdc  10481  brdom7disj  10491  brdom6disj  10492  uniimadom  10504  ondomon  10523  alephval2  10532  alephreg  10542  pwcfsdom  10543  elgch  10582  gchi  10584  fpwwe2lem11  10601  fpwwe2lem12  10602  winainflem  10653  winalim2  10656  tsken  10714  0tsk  10715  inar1  10735  tskord  10740  tskuni  10743  grudomon  10777  pinq  10887  nqereu  10889  enqeq  10894  ltbtwnnq  10938  ltrnq  10939  prcdnq  10953  prnmax  10955  genpnmax  10967  nqpr  10974  1idpr  10989  reclem2pr  11008  reclem3pr  11009  reclem4pr  11010  recexpr  11011  supexpr  11014  ltsosr  11054  1ne0sr  11056  ltasr  11060  supsrlem  11071  axpre-lttri  11125  axpre-lttrn  11126  axpre-ltadd  11127  axpre-sup  11129  lelttr  11271  dedekind  11344  dedekindle  11345  ltordlem  11710  lt0ne0d  11750  fimaxre3  12136  fiminre2  12138  lbreu  12140  lble  12142  sup2  12146  infm3  12149  suprleub  12156  supaddc  12157  supadd  12158  supmul1  12159  supmullem1  12160  supmul  12162  nnne0  12227  nnsub  12237  nominpos  12426  nnunb  12445  arch  12446  nn0sub  12499  nn0n0n1ge2b  12518  nn0lt10b  12603  zextle  12614  peano5uzti  12631  fzind  12639  btwnz  12644  uzval  12802  uzwo  12877  nnwof  12880  ublbneg  12899  lbzbi  12902  zsupss  12903  uzsupss  12906  uzwo3  12909  zmax  12911  rebtwnz  12913  rpnnen1lem3  12945  xrltnsym  13104  xrlttri  13106  xrlttr  13107  xrlelttr  13123  nltpnft  13131  xrmaxlt  13148  xrmaxle  13150  qbtwnre  13166  qbtwnxr  13167  xltnegi  13183  xnn0lenn0nn0  13212  xsubge0  13228  xlesubadd  13230  xmullem2  13232  xlemul1a  13255  xrinfmexpnf  13273  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  supxrunb1  13286  supxrunb2  13287  reltre  13308  rpltrp  13309  reltxrnmnf  13310  ixxval  13321  elixx1  13322  elioo2  13354  iccid  13358  icc0  13361  fzval  13477  elfz1  13480  elfznelfzo  13740  elfznelfzob  13741  flval  13763  fllelt  13766  flflp1  13776  flval2  13783  flval3  13784  flbi  13785  dfceil2  13808  ceilval2  13809  fleqceilz  13823  modid2  13867  addmodlteq  13918  fsequb2  13948  ssnn0fi  13957  seqf1olem2  14014  sqlecan  14181  faclbnd4lem1  14265  hashsnle1  14389  pr2pwpr  14451  hash3tpde  14465  rtrclreclem3  15033  relexpindlem  15036  sgnval  15061  01sqrexlem6  15220  01sqrex  15222  abslt  15288  absle  15289  rexanre  15320  rexico  15327  limsupgle  15450  limsupgre  15454  limsupbnd2  15456  rlim2lt  15470  rlim3  15471  ello12r  15490  ello1d  15496  elo12r  15501  rlimconst  15517  climshft  15549  rlimcn3  15563  o1rlimmul  15592  lo1le  15625  climsup  15643  caucvgrlem  15646  isumless  15818  divrcnv  15825  cvgrat  15856  rpnnen2lem10  16198  ruclem1  16206  ruclem2  16207  ruclem11  16215  ruclem12  16216  sqrt2irr  16224  absdvdsb  16251  dvdsle  16287  dvdsabseq  16290  dvdsdivcl  16293  dvdsext  16298  divalglem8  16377  divalglem9  16378  divalglem10  16379  divalgmod  16383  ndvdssub  16386  sadcaddlem  16434  gcdcllem1  16476  gcdcllem2  16477  gcdcllem3  16478  dfgcd2  16523  gcdzeq  16529  dvdssq  16544  nn0seqcvgd  16547  algcvgblem  16554  lcmval  16569  lcmdvds  16585  lcmgcdeq  16589  lcmfpr  16604  lcmf  16610  lcmftp  16613  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfdvdsb  16620  coprmgcdb  16626  coprmdvds1  16629  1nprm  16656  1idssfct  16657  isprm2lem  16658  isprm2  16659  dvdsprime  16664  nprm  16665  3prm  16671  dvdsprm  16680  exprmfct  16681  isprm5  16684  maxprmfct  16686  coprm  16688  prmdvdsncoprmbd  16704  ncoprmlnprm  16705  eulerthlem2  16759  phisum  16768  odzval  16769  pythagtriplem4  16797  pc2dvds  16857  pcprmpw2  16860  pcprmpw  16861  dvdsprmpweqle  16864  oddprmdvds  16881  prmpwdvds  16882  pockthg  16884  unbenlem  16886  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  1arith  16905  vdwlem6  16964  vdwlem11  16969  vdwlem13  16971  ramtlecl  16978  ramub  16991  rami  16993  ramubcl  16996  0ram  16998  ram0  17000  prmdvdsprmop  17021  prmolefac  17024  prmodvdslcmf  17025  prmgaplem2  17028  prmgaplcmlem1  17029  prmgaplcmlem2  17030  prmgaplem3  17031  prmgaplem4  17032  prmgaplem5  17033  prmgaplem6  17034  prmgapprmolem  17039  prmlem0  17083  prmlem1a  17084  imasaddfnlem  17498  imasvscafn  17507  imasleval  17511  prslem  18265  drsdir  18270  drsdirfi  18273  isdrs2  18274  posi  18285  posasymb  18287  pospropd  18293  pltval3  18305  plelttr  18310  pospo  18311  lubprop  18324  luble  18325  lublecllem  18326  glbprop  18337  joinval2lem  18346  joinlem  18349  meetlem  18363  meetle  18366  poslubmo  18377  posglbmo  18378  poslubd  18379  tleile  18387  latnlej  18422  isglbd  18475  lubub  18477  lubun  18481  clatleglb  18484  tsrlin  18551  letsr  18559  dirge  18569  pmtrval  19388  pmtrrn  19394  pmtrfrn  19395  pmtrrn2  19397  pmtrsn  19456  mndodcongi  19480  odeq  19487  odmulgeq  19494  gexnnod  19525  sylow1lem1  19535  pgpssslw  19551  sylow2a  19556  efgredeu  19689  efgred2  19690  gexex  19790  frgpnabllem2  19811  cyggenod  19821  dprdval  19942  dprdw  19949  dprdwd  19950  ablfacrplem  20004  ablfac1c  20010  ablfac1eu  20012  ablfaclem3  20026  abvtrivd  20748  zringlpir  21384  prmirredlem  21389  znleval  21471  frlmelbas  21672  ellspd  21718  islindf4  21754  psrbagconcl  21843  psrbagleadd1  21844  gsumbagdiaglem  21846  rhmpsrlem2  21857  psrlidm  21878  psrridm  21879  psrass1  21880  psrcom  21884  mplelbas  21907  mplmonmul  21950  ltbwe  21958  mhpmulcl  22043  psdmul  22060  coe1fsupp  22106  coe1ae0  22108  coe1mul2  22162  coe1tmmul  22170  pmatcoe1fsupp  22595  chfacffsupp  22750  chfacfscmulfsupp  22753  chfacfscmulgsum  22754  chfacfpmmulfsupp  22757  chfacfpmmulgsum  22758  ordtbas2  23085  ordtopn2  23089  ordtrest2lem  23097  pnfnei  23114  ordtt1  23273  ordthauslem  23277  2ndci  23342  2ndcsb  23343  2ndcredom  23344  2ndc1stc  23345  1stcrest  23347  2ndcctbss  23349  2ndcdisj  23350  2ndcsep  23353  lly1stc  23390  tx1stc  23544  ordthmeolem  23695  ufildom1  23820  xmetrtri2  24251  prdsxmetlem  24263  ssblex  24323  prdsbl  24386  comet  24408  stdbdxmet  24410  stdbdmopn  24413  met1stc  24416  dscmet  24467  metdstri  24747  metdscn  24752  xrhmeo  24851  bndth  24864  evth  24865  lebnumlem3  24869  pcovalg  24919  pco1  24922  pcocn  24924  pcopt  24929  pcopt2  24930  pcoass  24931  nmoleub3  25026  bcthlem5  25235  rrxfsupp  25309  minveclem4c  25332  minveclem2  25333  minveclem3b  25335  minveclem4  25339  minveclem6  25341  pmltpclem1  25356  pmltpc  25358  ovollb2lem  25396  ovolctb  25398  ovolunlem1  25405  ovoliunlem1  25410  ovoliunlem2  25411  ovoliun2  25414  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem3  25427  voliunlem2  25459  voliunlem3  25460  ioombl1lem4  25469  uniioovol  25487  uniioombllem2  25491  uniioombllem3  25493  uniioombllem6  25496  volsup2  25513  ismbfd  25547  mbfsup  25572  mbflimsup  25574  itg1climres  25622  mbfi1fseqlem4  25626  itg2lr  25638  itg2leub  25642  itg2seq  25650  itg2monolem1  25658  itg2monolem3  25660  itg2mono  25661  itg2i1fseq2  25664  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  itg2cn  25671  iblss  25713  itgless  25725  ibladdlem  25728  iblabsr  25738  iblmulc2  25739  itgabs  25743  bddiblnc  25750  ditgeq1  25756  dvferm2lem  25897  rolle  25901  dvlip2  25907  c1liplem1  25908  c1lip1  25909  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem4  25943  mdegleb  25976  degltlem1  25984  plyco0  26104  plyeq0lem  26122  coeeq2  26154  dgrle  26155  dgradd2  26181  plydiveu  26213  aareccl  26241  aalioulem2  26248  aaliou3lem7  26264  psercnlem1  26342  pilem2  26369  pilem3  26370  logltb  26516  divlogrlim  26551  logcnlem3  26560  cxpaddlelem  26668  rlimcnp  26882  cxplim  26889  cxploglim  26895  scvxcvx  26903  ftalem1  26990  ftalem2  26991  isppw2  27032  vmappw  27033  sgmnncl  27064  sqff1o  27099  fsumdvdsdiaglem  27100  dvdsppwf1o  27103  dvdsflsumcom  27105  musum  27108  muinv  27110  mpodvdsmulf1o  27111  dvdsmulf1o  27113  vmalelog  27123  vmasum  27134  logfac2  27135  perfectlem2  27148  bcmono  27195  bpos1lem  27200  bposlem9  27210  lgsmod  27241  lgsne0  27253  gausslemma2dlem4  27287  2sqlem6  27341  2sqlem8  27344  2sqlem10  27346  2sqreulem1  27364  2sqreunnlem1  27367  chtppilim  27393  rpvmasumlem  27405  dchrisumlema  27406  dchrisumlem2  27408  dchrvmasumlem1  27413  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0  27438  rplogsum  27445  logsqvma  27460  pntpbnd1  27504  pntpbnd2  27505  pntibndlem3  27510  pntlemj  27521  pntlemi  27522  pntlem3  27527  pnt3  27530  ostth3  27556  nodense  27611  noresle  27616  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupdm  27623  nosupbnd1lem1  27627  nosupbnd1lem4  27630  nosupbnd1  27633  nosupbnd2lem1  27634  nosupbnd2  27635  noinfcbv  27636  noinfdm  27638  noinffv  27640  noinfres  27641  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noinfbnd1  27648  noetalem2  27661  nocvxminlem  27696  ssltsepc  27712  conway  27718  scutval  27719  etasslt  27732  slerec  27738  bday1s  27750  cuteq1  27753  madeval2  27768  rightval  27779  elleft  27780  ssltright  27790  made0  27792  madecut  27801  left1s  27813  madebdaylemlrcut  27817  sltlpss  27826  cofsslt  27833  coinitsslt  27834  cofcutr  27839  cofcutrtime  27842  cofss  27845  coiniss  27846  cutmax  27849  cutmin  27850  addsproplem1  27883  addsprop  27890  sleadd1  27903  addsuniflem  27915  negsproplem1  27941  negsprop  27948  negsid  27954  negsunif  27968  mulsproplemcbv  28025  mulsproplem1  28026  mulsproplem9  28034  mulsprop  28040  ssltmul1  28057  ssltmul2  28058  mulsuniflem  28059  precsexlem11  28126  absslt  28158  onscutlt  28172  onsiso  28176  bdayon  28180  n0sfincut  28253  onsfi  28254  n0subs  28260  bdayn0p1  28265  eucliddivs  28272  zscut  28302  twocut  28316  halfcut  28340  addhalfcut  28341  elreno  28353  tgjustc1  28409  tgjustc2  28410  iscgrglt  28448  tgcgr4  28465  hlcgreu  28552  lmif  28719  islmib  28721  trgcopyeu  28740  iscgrad  28745  inaghl  28779  axlowdim2  28894  axlowdim  28895  axcontlem2  28899  axcontlem3  28900  axcontlem4  28901  axcontlem7  28904  axcontlem9  28906  axcontlem10  28907  axcontlem11  28908  axcontlem12  28909  ebtwntg  28916  umgrupgr  29037  nbusgrvtxm1  29313  crctcshwlkn0lem2  29748  crctcshwlkn0lem3  29749  crctcsh  29761  wlkswwlksf1o  29816  clwlkclwwlklem2fv1  29931  clwlkclwwlkf  29944  0clwlkv  30067  eupth2  30175  numclwwlk5  30324  nmoubi  30708  minvecolem2  30811  minvecolem3  30812  minvecolem4c  30815  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  htthlem  30853  chlimi  31170  chcompl  31178  hsn0elch  31184  cmbr3  31544  cmcm  31550  cmcm3  31551  lecm  31553  nmopub  31844  nmfnleub  31861  nmopun  31950  nmcexi  31962  cnlnadjlem7  32009  pjnmopi  32084  stle0i  32175  stlesi  32177  stm1i  32179  csmdsymi  32270  cvmd  32272  atcveq0  32284  atcv1  32316  atord  32324  atcvat2  32325  chirred  32331  mdsym  32348  mddmdin0i  32367  cdj1i  32369  fmptcof2  32588  fnpreimac  32602  isoun  32632  fcobijfs  32653  lt2addrd  32681  xlt2addrd  32689  xrge0infss  32690  infxrge0glb  32695  xrofsup  32697  fz1nnct  32733  sgnmulsgn  32774  toslublem  32905  tosglblem  32907  ismntd  32917  mgccole1  32923  mgccole2  32924  mgcmnt1  32925  mgcmnt2  32926  dfmgc2lem  32928  dfmgc2  32929  omndadd  33027  psgnfzto1stlem  33064  fzto1st  33067  psgnfzto1st  33069  trsp2cyc  33087  xrnarchi  33145  archirng  33149  archiexdiv  33151  archiabl  33159  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspn  33204  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrgspnsubrun  33207  isarchiofld  33302  linds2eq  33359  elrspunidl  33406  elrspunsn  33407  isrprm  33495  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1degltdimlem  33625  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  fldextrspunlsplem  33675  fldextrspunlsp  33676  smatrcl  33793  smatlem  33794  madjusmdetlem2  33825  madjusmdet  33828  cmpcref  33847  ldlfcntref  33851  dispcmp  33856  zarcmplem  33878  ordtrest2NEWlem  33919  ordtconnlem1  33921  xrge0iifiso  33932  rge0scvg  33946  gsumesum  34056  esumfsup  34067  esumpinfval  34070  esumpcvgval  34075  esumcvg  34083  sigaclcu  34114  sigaclci  34129  unelsiga  34131  unelldsys  34155  sigapildsys  34159  ldgenpisyslem1  34160  fiunelros  34171  measvun  34206  voliune  34226  volfiniune  34227  oms0  34295  omssubaddlem  34297  omssubadd  34298  carsgsigalem  34313  carsgclctunlem2  34317  carsgclctun  34319  pmeasmono  34322  pmeasadd  34323  orvcval2  34457  dstfrvel  34472  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsv  34508  ballotlemsf1o  34512  breprexp  34631  tgoldbachgt  34661  bnj23  34715  bnj1185  34790  bnj1152  34995  bnj1418  35037  fnrelpredd  35086  loop1cycl  35131  umgr2cycl  35135  acycgrcycl  35141  dfdm5  35767  dfrn5  35768  wzel  35819  wsuclem  35820  brpprod  35880  brsset  35884  brbigcup  35893  dffix2  35900  elfuns  35910  brimageg  35922  brdomaing  35930  brrangeg  35931  brimg  35932  brapply  35933  brsuccf  35936  funpartlem  35937  brrestrict  35944  dfrecs2  35945  dfrdg4  35946  brofs  36000  btwncomim  36008  btwnintr  36014  btwnexch3  36015  btwnexch2  36018  brifs  36038  brcolinear2  36053  colineardim1  36056  brfs  36074  btwnconn1  36096  segcon2  36100  seglerflx  36107  seglemin  36108  btwnsegle  36112  colinbtwnle  36113  broutsideof2  36117  fvray  36136  lineunray  36142  lineelsb2  36143  linerflx1  36144  trer  36311  elicc3  36312  finminlem  36313  nn0prpwlem  36317  nn0prpw  36318  fnessref  36352  refssfne  36353  weiunlem2  36458  weiunfrlem  36459  weiunfr  36462  weiunse  36463  unblimceq0lem  36501  unblimceq0  36502  unbdqndv2  36506  knoppndvlem21  36527  taupilemrplb  37315  dfgcd3  37319  icorempo  37346  icoreval  37348  iooelexlt  37357  relowlssretop  37358  domalom  37399  ctbssinf  37401  pibt2  37412  phpreu  37605  fin2solem  37607  fin2so  37608  ltflcei  37609  ptrecube  37621  poimirlem1  37622  poimirlem2  37623  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem9  37630  poimirlem12  37633  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  poimirlem32  37653  heicant  37656  mblfinlem1  37658  mblfinlem2  37659  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ibladdnclem  37677  iblmulc2nc  37686  itgabsnc  37690  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  indexdom  37735  filbcmb  37741  fdc  37746  prdsbnd  37794  heiborlem3  37814  rrnequiv  37836  rngoueqz  37941  eqbrtr  38227  elrnressn  38269  inxprnres  38287  eqvreltr  38605  prtlem10  38865  lsatcveq0  39032  lsatcv1  39048  oposlem  39182  opnlen0  39188  lub0N  39189  glb0N  39193  omllaw  39243  cmtbr4N  39255  cvrval  39269  cvrnbtwn  39271  cvrnbtwn2  39275  cvrnbtwn3  39276  cvrcon3b  39277  cvrnbtwn4  39279  atcvreq0  39314  atnle  39317  atlatmstc  39319  cvlexch1  39328  glbconN  39377  glbconNOLD  39378  hlsuprexch  39382  exatleN  39405  cvratlem  39422  atcvrj0  39429  atcvrj2b  39433  atlelt  39439  cvrat4  39444  3dim1lem5  39467  3dim2  39469  3dim3  39470  ps-2  39479  llni  39509  llnn0  39517  llnle  39519  lplni  39533  lplni2  39538  lplnle  39541  lplnn0N  39548  llncvrlpln  39559  2llnjN  39568  lvoli  39576  lvoli3  39578  lvoli2  39582  lvoln0N  39592  4at  39614  lplncvrlvol  39617  2lplnj  39621  dalemcea  39661  dalem3  39665  psubspi  39748  linepsubN  39753  elpmap  39759  pmapsub  39769  lnatexN  39780  cdlema1N  39792  cdlemb  39795  elpadd  39800  paddvaln0N  39802  paddasslem5  39825  llnexchb2lem  39869  llnexch2N  39871  islhp  39997  lhpat3  40047  4atexlemex2  40072  4atex  40077  4atex2-0aOLDN  40079  4atex2-0cOLDN  40081  lautle  40085  lautcvr  40093  lauteq  40096  ldilval  40114  ltrnu  40122  trlval2  40164  trlne  40186  cdleme0ex1N  40224  cdleme0nex  40291  cdleme18d  40296  cdlemednuN  40301  cdleme25b  40355  cdleme25cv  40359  cdleme27b  40369  cdleme29b  40376  cdleme31sn  40381  cdleme31fv  40391  cdleme31fv2  40394  cdlemefrs29bpre0  40397  cdlemefr29bpre0N  40407  cdlemefr29clN  40408  cdlemefr32fvaN  40410  cdlemefr32fva1  40411  cdlemefs29pre00N  40413  cdlemefs32sn1aw  40415  cdlemefs29bpre0N  40417  cdlemefs29bpre1N  40418  cdlemefs29cpre1N  40419  cdlemefs29clN  40420  cdlemefs32fvaN  40423  cdlemefs32fva1  40424  cdleme41sn3a  40434  cdleme32fva  40438  cdleme32e  40446  cdleme35f  40455  cdleme40v  40470  cdleme42b  40479  trlord  40570  cdlemg1cex  40589  diaval  41033  diaeldm  41037  diaelrnN  41046  cdlemm10N  41119  dibglbN  41167  dicval  41177  dicfnN  41184  dicvalrelN  41186  dihval  41233  dihlsscpre  41235  dihglblem3N  41296  dihmeetlem2N  41300  djhcvat42  41416  lcmineqlem4  42027  aks4d1p4  42074  aks4d1p5  42075  aks4d1p7  42078  aks4d1p8d2  42080  aks4d1p8  42082  hashnexinjle  42124  sticksstones1  42141  sticksstones2  42142  sticksstones10  42150  sticksstones12a  42152  aks6d1c7lem4  42178  aks6d1c7  42179  grpods  42189  unitscyglem2  42191  unitscyglem3  42192  unitscyglem4  42193  qsalrel  42235  supinf  42237  dvdsexpnn0  42329  redvmptabs  42355  sn-nnne0  42455  sn-sup2  42486  fimgmcyclem  42528  flt4lem2  42642  flt4lem7  42654  lzenom  42765  fphpdo  42812  irrapxlem4  42820  pellexlem6  42829  infmrgelbi  42873  pellfundre  42876  pellfundlb  42879  monotoddzz  42939  zindbi  42942  jm2.27  43004  rmydioph  43010  rpnnen3lem  43027  fnwe2lem2  43047  aomclem8  43057  hbtlem5  43124  hbt  43126  sdomne0  43409  sdomne0d  43410  ensucne0  43525  sucomisnotcard  43540  en2pr  43543  pr2cv  43544  refimssco  43603  rfovfvfvd  43999  rfovcnvf1od  44000  fsovrfovd  44005  nzss  44313  relprel  44948  permaxinf2lem  45009  wessf1ornlem  45186  axccdom  45223  dmrelrnrel  45227  axccd  45230  rnmptlb  45244  rnmptbdd  45246  rnmptbd2  45250  rnmptbdlem  45256  rnmptbd  45257  dstregt0  45287  suplesup  45342  supxrunb3  45402  supxrleubrnmpt  45409  rexabslelem  45421  rexabsle  45422  suprleubrnmpt  45425  infrnmptle  45426  infxrunb3rnmpt  45431  infxrpnf  45449  supminfxr  45467  infrpgernmpt  45468  xrpnf  45488  limsupre  45646  limsupref  45690  limsupbnd1f  45691  limsuppnfd  45707  climinf2  45712  limsuppnf  45716  climinfmpt  45720  climinf3  45721  limsupmnflem  45725  limsupmnf  45726  limsupre2  45730  limsupmnfuzlem  45731  limsupre2mpt  45735  limsupre3lem  45737  limsupre3  45738  limsupre3mpt  45739  limsupre3uzlem  45740  limsupre3uz  45741  limsupreuz  45742  limsupreuzmpt  45744  liminfval2  45773  liminfreuzlem  45807  liminfreuz  45808  xlimpnfxnegmnf  45819  cnrefiisplem  45834  xlimpnfv  45843  xlimpnf  45847  xlimpnfmpt  45849  dfxlim2  45853  icccncfext  45892  cncficcgt0  45893  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem5  46010  stoweidlem20  46025  stoweidlem26  46031  stoweidlem28  46033  stoweidlem29  46034  stoweidlem34  46039  wallispilem3  46072  stirlinglem13  46091  fourierdlem41  46153  fourierdlem42  46154  fourierdlem51  46162  fourierdlem54  46165  salunicl  46321  saluncl  46322  salexct  46339  salexct2  46344  salexct3  46347  salgencntex  46348  salgensscntex  46349  sge0pnffigt  46401  meadjuni  46462  omeunile  46510  ovnlerp  46567  hoidifhspval  46613  ovolval5lem2  46658  salpreimagelt  46712  pimincfltioo  46723  salpreimagtge  46730  salpreimagtlt  46735  incsmf  46747  issmfgt  46761  smfpreimagt  46767  decsmf  46772  issmfge  46775  smfpimgtxr  46785  smfpreimage  46787  smfinflem  46822  smfinf  46823  finfdm  46851  funressnfv  47048  funressnvmo  47050  funressnmo  47051  dfdfat2  47133  tz6.12-afv  47178  funressndmafv2rn  47228  tz6.12-afv2  47245  dfatcolem  47260  dfatco  47261  zplusmodne  47348  m1modne  47353  minusmod5ne  47354  submodneaddmod  47356  modmknepk  47367  iccpartigtl  47428  iccpartgt  47432  icceuelpartlem  47440  iccpartnel  47443  sprsymrelfolem2  47498  goldbachthlem2  47551  odz2prm2pw  47568  fmtnoprmfac1  47570  fmtnoprmfac2  47572  fmtnofac2  47574  fmtno4prmfac  47577  fmtno4prm  47580  prmdvdsfmtnof1lem1  47589  31prm  47602  perfectALTVlem2  47727  nnsum3primes4  47793  nnsum3primesprm  47795  nnsum3primesgbe  47797  nnsum3primesle9  47799  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem4  47813  bgoldbtbnd  47814  tgblthelfgott  47820  tgoldbach  47822  assintop  48201  isassintop  48202  assintopcllaw  48204  ztprmneprm  48339  ply1mulgsumlem1  48379  ply1mulgsumlem2  48380  lco0  48420  lcoel0  48421  lincsumcl  48424  lincscmcl  48425  lcoss  48429  linindslinci  48441  lindslinindsimp1  48450  linds0  48458  el0ldep  48459  lindsrng01  48461  ldepspr  48466  islindeps2  48476  isldepslvec2  48478  zlmodzxzldep  48497  ldepsnlinc  48501  elbigo2r  48546  xpco2  48849  tposres0  48869  lubsscl  48952  glbsscl  48953  lubprlem  48954  ipolub  48980  ipoglb  48983  catprslem  49003  infsubc2  49054  nelsubc3lem  49063  cnelsubclem  49596  setrec2lem1  49686