Theorem breq1 5146

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ⟨cop 4632   class class class wbr 5143

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  breq12  5148  breq1i  5150  breq1d  5153  nbrne2  5163  brab1  5191  pocl  5600  swopolem  5602  swopo  5603  po2ne  5608  solin  5619  sotrieq  5623  sotr2  5626  isso2i  5629  somo  5631  dffr2  5646  frc  5648  frirr  5661  fr2nr  5662  wereu2  5682  vtoclr  5748  frsn  5773  brcog  5877  brcogw  5879  brcnvg  5890  dfdmf  5907  eldmg  5909  dfrnf  5961  dmcosseq  5987  dfres2  6059  imasng  6102  cotrg  6127  cnvsym  6132  asymref2  6137  sotri2  6149  somin1  6153  coi1  6282  predtrss  6343  frpomin  6361  dffun2  6571  dffun6f  6579  funmo  6581  funmoOLD  6582  fun11  6640  fveq2  6906  eliman0  6946  nfunsn  6948  dffv2  7004  fvopab5  7049  dff3  7120  f1ompt  7131  fmptco  7149  dff13  7275  foeqcnvco  7320  isorel  7346  soisores  7347  soisoi  7348  isocnv  7350  isotr  7356  isomin  7357  isoini  7358  isopolem  7365  isosolem  7367  f1oiso  7371  f1oiso2  7372  weniso  7374  eqfunresadj  7380  caovordig  7638  caovordg  7640  caovord3d  7643  caovord  7644  caovord3  7646  caofrss  7736  caoftrn  7738  fr3nr  7792  dfwe2  7794  f1oweALT  7997  frxp  8151  poxp  8153  fnse  8158  poxp2  8168  frxp2  8169  poxp3  8175  frxp3  8176  xpord3pred  8177  poseq  8183  brtpos2  8257  rntpos  8264  tpostpos  8271  frrlem12  8322  ertr  8760  ecopovsym  8859  ecopovtrn  8860  isfi  9016  en0  9058  en0ALT  9059  en1  9064  endisj  9098  xpcomco  9102  sbth  9133  2pwne  9173  disjenex  9175  ssenen  9191  findcard  9203  findcard2  9204  pssnn  9208  sbthfi  9239  nneneq  9246  php  9247  nneneqOLD  9258  phpOLD  9259  onomeneq  9265  sdom1  9278  sdom1OLD  9279  1sdom2dom  9283  isinf  9296  isinfOLD  9297  fineqvlem  9298  en1eqsnbi  9310  enp1iOLD  9314  findcard3  9318  findcard3OLD  9319  frfi  9321  fiint  9366  fiintOLD  9367  mapfienlem1  9445  mapfienlem2  9446  mapfienlem3  9447  mapfien  9448  marypha1lem  9473  supmo  9492  eqsup  9496  supub  9499  suplub  9500  suppr  9511  supisolem  9513  supisoex  9514  infmin  9534  infmo  9535  fiinfg  9539  fiinf2g  9540  infpr  9543  ordtypecbv  9557  ordtypelem3  9560  ordtypelem6  9563  ordtypelem7  9564  ordtypelem9  9566  ordtypelem10  9567  hartogslem1  9582  hartogs  9584  wemaplem1  9586  wemaplem2  9587  wemapso2lem  9592  card2on  9594  card2inf  9595  elharval  9601  brwdom2  9613  wdomtr  9615  cantnfs  9706  cantnfp1lem2  9719  oemapso  9722  cantnflem1  9729  wemapwe  9737  ttrclss  9760  r111  9815  kardex  9934  karden  9935  isnumi  9986  tskwe  9990  cardid2  9993  cardonle  9997  cardne  10005  iscard2  10016  infxpenlem  10053  fodomfi2  10100  wdomfil  10101  wdomnumr  10104  alephsuc2  10120  infenaleph  10131  iunfictbso  10154  infpss  10256  cff1  10298  cfslb2n  10308  sornom  10317  fin4i  10338  isfin6  10340  isfin7  10341  isfin1-3  10426  fin1a2lem9  10448  fin1a2lem11  10450  hsmexlem4  10469  axcc2lem  10476  axcc4dom  10481  domtriomlem  10482  numthcor  10534  zorn2lem2  10537  zorn2lem3  10538  zorn2lem7  10542  zorn2g  10543  axdclem  10559  axdc  10561  brdom7disj  10571  brdom6disj  10572  uniimadom  10584  ondomon  10603  alephval2  10612  alephreg  10622  pwcfsdom  10623  elgch  10662  gchi  10664  fpwwe2lem11  10681  fpwwe2lem12  10682  winainflem  10733  winalim2  10736  tsken  10794  0tsk  10795  inar1  10815  tskord  10820  tskuni  10823  grudomon  10857  pinq  10967  nqereu  10969  enqeq  10974  ltbtwnnq  11018  ltrnq  11019  prcdnq  11033  prnmax  11035  genpnmax  11047  nqpr  11054  1idpr  11069  reclem2pr  11088  reclem3pr  11089  reclem4pr  11090  recexpr  11091  supexpr  11094  ltsosr  11134  1ne0sr  11136  ltasr  11140  supsrlem  11151  axpre-lttri  11205  axpre-lttrn  11206  axpre-ltadd  11207  axpre-sup  11209  lelttr  11351  dedekind  11424  dedekindle  11425  ltordlem  11788  lt0ne0d  11828  fimaxre3  12214  fiminre2  12216  lbreu  12218  lble  12220  sup2  12224  infm3  12227  suprleub  12234  supaddc  12235  supadd  12236  supmul1  12237  supmullem1  12238  supmul  12240  nnne0  12300  nnsub  12310  nominpos  12503  nnunb  12522  arch  12523  nn0sub  12576  nn0n0n1ge2b  12595  nn0lt10b  12680  zextle  12691  peano5uzti  12708  fzind  12716  btwnz  12721  uzval  12880  uzwo  12953  nnwof  12956  ublbneg  12975  lbzbi  12978  zsupss  12979  uzsupss  12982  uzwo3  12985  zmax  12987  rebtwnz  12989  rpnnen1lem3  13021  xrltnsym  13179  xrlttri  13181  xrlttr  13182  xrlelttr  13198  nltpnft  13206  xrmaxlt  13223  xrmaxle  13225  qbtwnre  13241  qbtwnxr  13242  xltnegi  13258  xnn0lenn0nn0  13287  xsubge0  13303  xlesubadd  13305  xmullem2  13307  xlemul1a  13330  xrinfmexpnf  13348  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  supxrunb1  13361  supxrunb2  13362  reltre  13382  rpltrp  13383  reltxrnmnf  13384  ixxval  13395  elixx1  13396  elioo2  13428  iccid  13432  icc0  13435  fzval  13549  elfz1  13552  elfznelfzo  13811  elfznelfzob  13812  flval  13834  fllelt  13837  flflp1  13847  flval2  13854  flval3  13855  flbi  13856  dfceil2  13879  ceilval2  13880  fleqceilz  13894  modid2  13938  addmodlteq  13987  fsequb2  14017  ssnn0fi  14026  seqf1olem2  14083  sqlecan  14248  faclbnd4lem1  14332  hashsnle1  14456  pr2pwpr  14518  hash3tpde  14532  rtrclreclem3  15099  relexpindlem  15102  sgnval  15127  01sqrexlem6  15286  01sqrex  15288  abslt  15353  absle  15354  rexanre  15385  rexico  15392  limsupgle  15513  limsupgre  15517  limsupbnd2  15519  rlim2lt  15533  rlim3  15534  ello12r  15553  ello1d  15559  elo12r  15564  rlimconst  15580  climshft  15612  rlimcn3  15626  o1rlimmul  15655  lo1le  15688  climsup  15706  caucvgrlem  15709  isumless  15881  divrcnv  15888  cvgrat  15919  rpnnen2lem10  16259  ruclem1  16267  ruclem2  16268  ruclem11  16276  ruclem12  16277  sqrt2irr  16285  absdvdsb  16312  dvdsle  16347  dvdsabseq  16350  dvdsdivcl  16353  dvdsext  16358  divalglem8  16437  divalglem9  16438  divalglem10  16439  divalgmod  16443  ndvdssub  16446  sadcaddlem  16494  gcdcllem1  16536  gcdcllem2  16537  gcdcllem3  16538  dfgcd2  16583  gcdzeq  16589  dvdssq  16604  nn0seqcvgd  16607  algcvgblem  16614  lcmval  16629  lcmdvds  16645  lcmgcdeq  16649  lcmfpr  16664  lcmf  16670  lcmftp  16673  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfdvdsb  16680  coprmgcdb  16686  coprmdvds1  16689  1nprm  16716  1idssfct  16717  isprm2lem  16718  isprm2  16719  dvdsprime  16724  nprm  16725  3prm  16731  dvdsprm  16740  exprmfct  16741  isprm5  16744  maxprmfct  16746  coprm  16748  prmdvdsncoprmbd  16764  ncoprmlnprm  16765  eulerthlem2  16819  phisum  16828  odzval  16829  pythagtriplem4  16857  pc2dvds  16917  pcprmpw2  16920  pcprmpw  16921  dvdsprmpweqle  16924  oddprmdvds  16941  prmpwdvds  16942  pockthg  16944  unbenlem  16946  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  1arith  16965  vdwlem6  17024  vdwlem11  17029  vdwlem13  17031  ramtlecl  17038  ramub  17051  rami  17053  ramubcl  17056  0ram  17058  ram0  17060  prmdvdsprmop  17081  prmolefac  17084  prmodvdslcmf  17085  prmgaplem2  17088  prmgaplcmlem1  17089  prmgaplcmlem2  17090  prmgaplem3  17091  prmgaplem4  17092  prmgaplem5  17093  prmgaplem6  17094  prmgapprmolem  17099  prmlem0  17143  prmlem1a  17144  imasaddfnlem  17573  imasvscafn  17582  imasleval  17586  prslem  18343  drsdir  18348  drsdirfi  18351  isdrs2  18352  posi  18363  posasymb  18365  pospropd  18372  pltval3  18384  plelttr  18389  pospo  18390  lubprop  18403  luble  18404  lublecllem  18405  glbprop  18416  joinval2lem  18425  joinlem  18428  meetlem  18442  meetle  18445  poslubmo  18456  posglbmo  18457  poslubd  18458  tleile  18466  latnlej  18501  isglbd  18554  lubub  18556  lubun  18560  clatleglb  18563  tsrlin  18630  letsr  18638  dirge  18648  pmtrval  19469  pmtrrn  19475  pmtrfrn  19476  pmtrrn2  19478  pmtrsn  19537  mndodcongi  19561  odeq  19568  odmulgeq  19575  gexnnod  19606  sylow1lem1  19616  pgpssslw  19632  sylow2a  19637  efgredeu  19770  efgred2  19771  gexex  19871  frgpnabllem2  19892  cyggenod  19902  dprdval  20023  dprdw  20030  dprdwd  20031  ablfacrplem  20085  ablfac1c  20091  ablfac1eu  20093  ablfaclem3  20107  abvtrivd  20833  zringlpir  21478  prmirredlem  21483  znleval  21573  frlmelbas  21776  ellspd  21822  islindf4  21858  psrbagconcl  21947  psrbagleadd1  21948  gsumbagdiaglem  21950  rhmpsrlem2  21961  psrlidm  21982  psrridm  21983  psrass1  21984  psrcom  21988  mplelbas  22011  mplmonmul  22054  ltbwe  22062  mhpmulcl  22153  psdmul  22170  coe1fsupp  22216  coe1ae0  22218  coe1mul2  22272  coe1tmmul  22280  pmatcoe1fsupp  22707  chfacffsupp  22862  chfacfscmulfsupp  22865  chfacfscmulgsum  22866  chfacfpmmulfsupp  22869  chfacfpmmulgsum  22870  ordtbas2  23199  ordtopn2  23203  ordtrest2lem  23211  pnfnei  23228  ordtt1  23387  ordthauslem  23391  2ndci  23456  2ndcsb  23457  2ndcredom  23458  2ndc1stc  23459  1stcrest  23461  2ndcctbss  23463  2ndcdisj  23464  2ndcsep  23467  lly1stc  23504  tx1stc  23658  ordthmeolem  23809  ufildom1  23934  xmetrtri2  24366  prdsxmetlem  24378  ssblex  24438  prdsbl  24504  comet  24526  stdbdxmet  24528  stdbdmopn  24531  met1stc  24534  dscmet  24585  metdstri  24873  metdscn  24878  xrhmeo  24977  bndth  24990  evth  24991  lebnumlem3  24995  pcovalg  25045  pco1  25048  pcocn  25050  pcopt  25055  pcopt2  25056  pcoass  25057  nmoleub3  25152  bcthlem5  25362  rrxfsupp  25436  minveclem4c  25459  minveclem2  25460  minveclem3b  25462  minveclem4  25466  minveclem6  25468  pmltpclem1  25483  pmltpc  25485  ovollb2lem  25523  ovolctb  25525  ovolunlem1  25532  ovoliunlem1  25537  ovoliunlem2  25538  ovoliun2  25541  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem3  25554  voliunlem2  25586  voliunlem3  25587  ioombl1lem4  25596  uniioovol  25614  uniioombllem2  25618  uniioombllem3  25620  uniioombllem6  25623  volsup2  25640  ismbfd  25674  mbfsup  25699  mbflimsup  25701  itg1climres  25749  mbfi1fseqlem4  25753  itg2lr  25765  itg2leub  25769  itg2seq  25777  itg2monolem1  25785  itg2monolem3  25787  itg2mono  25788  itg2i1fseq2  25791  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  itg2cn  25798  iblss  25840  itgless  25852  ibladdlem  25855  iblabsr  25865  iblmulc2  25866  itgabs  25870  bddiblnc  25877  ditgeq1  25883  dvferm2lem  26024  rolle  26028  dvlip2  26034  c1liplem1  26035  c1lip1  26036  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  mdegleb  26103  degltlem1  26111  plyco0  26231  plyeq0lem  26249  coeeq2  26281  dgrle  26282  dgradd2  26308  plydiveu  26340  aareccl  26368  aalioulem2  26375  aaliou3lem7  26391  psercnlem1  26469  pilem2  26496  pilem3  26497  logltb  26642  divlogrlim  26677  logcnlem3  26686  cxpaddlelem  26794  rlimcnp  27008  cxplim  27015  cxploglim  27021  scvxcvx  27029  ftalem1  27116  ftalem2  27117  isppw2  27158  vmappw  27159  sgmnncl  27190  sqff1o  27225  fsumdvdsdiaglem  27226  dvdsppwf1o  27229  dvdsflsumcom  27231  musum  27234  muinv  27236  mpodvdsmulf1o  27237  dvdsmulf1o  27239  vmalelog  27249  vmasum  27260  logfac2  27261  perfectlem2  27274  bcmono  27321  bpos1lem  27326  bposlem9  27336  lgsmod  27367  lgsne0  27379  gausslemma2dlem4  27413  2sqlem6  27467  2sqlem8  27470  2sqlem10  27472  2sqreulem1  27490  2sqreunnlem1  27493  chtppilim  27519  rpvmasumlem  27531  dchrisumlema  27532  dchrisumlem2  27534  dchrvmasumlem1  27539  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0  27564  rplogsum  27571  logsqvma  27586  pntpbnd1  27630  pntpbnd2  27631  pntibndlem3  27636  pntlemj  27647  pntlemi  27648  pntlem3  27653  pnt3  27656  ostth3  27682  nodense  27737  noresle  27742  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupdm  27749  nosupbnd1lem1  27753  nosupbnd1lem4  27756  nosupbnd1  27759  nosupbnd2lem1  27760  nosupbnd2  27761  noinfcbv  27762  noinfdm  27764  noinffv  27766  noinfres  27767  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noinfbnd1  27774  noetalem2  27787  nocvxminlem  27822  ssltsepc  27838  conway  27844  scutval  27845  etasslt  27858  slerec  27864  bday1s  27876  cuteq1  27878  madeval2  27892  rightval  27903  ssltright  27910  made0  27912  madecut  27921  left1s  27933  madebdaylemlrcut  27937  sltlpss  27945  0elleft  27948  cofsslt  27952  coinitsslt  27953  cofcutr  27958  cofcutrtime  27961  cofss  27964  coiniss  27965  cutmax  27968  cutmin  27969  addsproplem1  28002  addsproplem4  28005  addsproplem6  28007  addsprop  28009  sleadd1  28022  addsuniflem  28034  negsproplem1  28060  negsproplem4  28063  negsprop  28067  negsid  28073  negsunif  28087  mulsproplemcbv  28141  mulsproplem1  28142  mulsproplem9  28150  mulsproplem12  28153  mulsprop  28156  ssltmul1  28173  ssltmul2  28174  mulsuniflem  28175  precsexlem9  28239  precsexlem11  28241  absslt  28273  sltonold  28283  n0subs  28360  zscut  28393  nohalf  28407  halfcut  28416  addhalfcut  28419  elreno  28427  tgjustc1  28483  tgjustc2  28484  iscgrglt  28522  tgcgr4  28539  hlcgreu  28626  lmif  28793  islmib  28795  trgcopyeu  28814  iscgrad  28819  inaghl  28853  axlowdim2  28975  axlowdim  28976  axcontlem2  28980  axcontlem3  28981  axcontlem4  28982  axcontlem7  28985  axcontlem9  28987  axcontlem10  28988  axcontlem11  28989  axcontlem12  28990  ebtwntg  28997  umgrupgr  29120  nbusgrvtxm1  29396  crctcshwlkn0lem2  29831  crctcshwlkn0lem3  29832  crctcsh  29844  wlkswwlksf1o  29899  clwlkclwwlklem2fv1  30014  clwlkclwwlkf  30027  0clwlkv  30150  eupth2  30258  numclwwlk5  30407  nmoubi  30791  minvecolem2  30894  minvecolem3  30895  minvecolem4c  30898  minvecolem4  30899  minvecolem5  30900  minvecolem6  30901  htthlem  30936  chlimi  31253  chcompl  31261  hsn0elch  31267  cmbr3  31627  cmcm  31633  cmcm3  31634  lecm  31636  nmopub  31927  nmfnleub  31944  nmopun  32033  nmcexi  32045  cnlnadjlem7  32092  pjnmopi  32167  stle0i  32258  stlesi  32260  stm1i  32262  csmdsymi  32353  cvmd  32355  atcveq0  32367  atcv1  32399  atord  32407  atcvat2  32408  chirred  32414  mdsym  32431  mddmdin0i  32450  cdj1i  32452  fmptcof2  32667  fnpreimac  32681  isoun  32711  fcobijfs  32734  lt2addrd  32755  xlt2addrd  32762  xrge0infss  32764  infxrge0glb  32769  xrofsup  32771  fz1nnct  32805  toslublem  32962  tosglblem  32964  ismntd  32974  mgccole1  32980  mgccole2  32981  mgcmnt1  32982  mgcmnt2  32983  dfmgc2lem  32985  dfmgc2  32986  omndadd  33083  psgnfzto1stlem  33120  fzto1st  33123  psgnfzto1st  33125  trsp2cyc  33143  xrnarchi  33191  archirng  33195  archiexdiv  33197  archiabl  33205  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspn  33250  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  isarchiofld  33347  linds2eq  33409  elrspunidl  33456  elrspunsn  33457  isrprm  33545  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  ply1degltdimlem  33673  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  fldextrspunlsplem  33723  fldextrspunlsp  33724  smatrcl  33795  smatlem  33796  madjusmdetlem2  33827  madjusmdet  33830  cmpcref  33849  ldlfcntref  33853  dispcmp  33858  zarcmplem  33880  ordtrest2NEWlem  33921  ordtconnlem1  33923  xrge0iifiso  33934  rge0scvg  33948  gsumesum  34060  esumfsup  34071  esumpinfval  34074  esumpcvgval  34079  esumcvg  34087  sigaclcu  34118  sigaclci  34133  unelsiga  34135  unelldsys  34159  sigapildsys  34163  ldgenpisyslem1  34164  fiunelros  34175  measvun  34210  voliune  34230  volfiniune  34231  oms0  34299  omssubaddlem  34301  omssubadd  34302  carsgsigalem  34317  carsgclctunlem2  34321  carsgclctun  34323  pmeasmono  34326  pmeasadd  34327  orvcval2  34461  dstfrvel  34476  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsv  34512  ballotlemsf1o  34516  sgnmulsgn  34552  breprexp  34648  tgoldbachgt  34678  bnj23  34732  bnj1185  34807  bnj1152  35012  bnj1418  35054  fnrelpredd  35103  loop1cycl  35142  umgr2cycl  35146  acycgrcycl  35152  dfdm5  35773  dfrn5  35774  wzel  35825  wsuclem  35826  brpprod  35886  brsset  35890  brbigcup  35899  dffix2  35906  elfuns  35916  brimageg  35928  brdomaing  35936  brrangeg  35937  brimg  35938  brapply  35939  brsuccf  35942  funpartlem  35943  brrestrict  35950  dfrecs2  35951  dfrdg4  35952  brofs  36006  btwncomim  36014  btwnintr  36020  btwnexch3  36021  btwnexch2  36024  brifs  36044  brcolinear2  36059  colineardim1  36062  brfs  36080  btwnconn1  36102  segcon2  36106  seglerflx  36113  seglemin  36114  btwnsegle  36118  colinbtwnle  36119  broutsideof2  36123  fvray  36142  lineunray  36148  lineelsb2  36149  linerflx1  36150  trer  36317  elicc3  36318  finminlem  36319  nn0prpwlem  36323  nn0prpw  36324  fnessref  36358  refssfne  36359  weiunlem2  36464  weiunfrlem  36465  weiunfr  36468  weiunse  36469  unblimceq0lem  36507  unblimceq0  36508  unbdqndv2  36512  knoppndvlem21  36533  taupilemrplb  37321  dfgcd3  37325  icorempo  37352  icoreval  37354  iooelexlt  37363  relowlssretop  37364  domalom  37405  ctbssinf  37407  pibt2  37418  phpreu  37611  fin2solem  37613  fin2so  37614  ltflcei  37615  ptrecube  37627  poimirlem1  37628  poimirlem2  37629  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem9  37636  poimirlem12  37639  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem32  37659  heicant  37662  mblfinlem1  37664  mblfinlem2  37665  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ibladdnclem  37683  iblmulc2nc  37692  itgabsnc  37696  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  indexdom  37741  filbcmb  37747  fdc  37752  prdsbnd  37800  heiborlem3  37820  rrnequiv  37842  rngoueqz  37947  eqbrtr  38233  elrnressn  38274  inxprnres  38293  eqvreltr  38608  prtlem10  38866  lsatcveq0  39033  lsatcv1  39049  oposlem  39183  opnlen0  39189  lub0N  39190  glb0N  39194  omllaw  39244  cmtbr4N  39256  cvrval  39270  cvrnbtwn  39272  cvrnbtwn2  39276  cvrnbtwn3  39277  cvrcon3b  39278  cvrnbtwn4  39280  atcvreq0  39315  atnle  39318  atlatmstc  39320  cvlexch1  39329  glbconN  39378  glbconNOLD  39379  hlsuprexch  39383  exatleN  39406  cvratlem  39423  atcvrj0  39430  atcvrj2b  39434  atlelt  39440  cvrat4  39445  3dim1lem5  39468  3dim2  39470  3dim3  39471  ps-2  39480  llni  39510  llnn0  39518  llnle  39520  lplni  39534  lplni2  39539  lplnle  39542  lplnn0N  39549  llncvrlpln  39560  2llnjN  39569  lvoli  39577  lvoli3  39579  lvoli2  39583  lvoln0N  39593  4at  39615  lplncvrlvol  39618  2lplnj  39622  dalemcea  39662  dalem3  39666  psubspi  39749  linepsubN  39754  elpmap  39760  pmapsub  39770  lnatexN  39781  cdlema1N  39793  cdlemb  39796  elpadd  39801  paddvaln0N  39803  paddasslem5  39826  llnexchb2lem  39870  llnexch2N  39872  islhp  39998  lhpat3  40048  4atexlemex2  40073  4atex  40078  4atex2-0aOLDN  40080  4atex2-0cOLDN  40082  lautle  40086  lautcvr  40094  lauteq  40097  ldilval  40115  ltrnu  40123  trlval2  40165  trlne  40187  cdleme0ex1N  40225  cdleme0nex  40292  cdleme18d  40297  cdlemednuN  40302  cdleme25b  40356  cdleme25cv  40360  cdleme27b  40370  cdleme29b  40377  cdleme31sn  40382  cdleme31fv  40392  cdleme31fv2  40395  cdlemefrs29bpre0  40398  cdlemefr29bpre0N  40408  cdlemefr29clN  40409  cdlemefr32fvaN  40411  cdlemefr32fva1  40412  cdlemefs29pre00N  40414  cdlemefs32sn1aw  40416  cdlemefs29bpre0N  40418  cdlemefs29bpre1N  40419  cdlemefs29cpre1N  40420  cdlemefs29clN  40421  cdlemefs32fvaN  40424  cdlemefs32fva1  40425  cdleme41sn3a  40435  cdleme32fva  40439  cdleme32e  40447  cdleme35f  40456  cdleme40v  40471  cdleme42b  40480  trlord  40571  cdlemg1cex  40590  diaval  41034  diaeldm  41038  diaelrnN  41047  cdlemm10N  41120  dibglbN  41168  dicval  41178  dicfnN  41185  dicvalrelN  41187  dihval  41234  dihlsscpre  41236  dihglblem3N  41297  dihmeetlem2N  41301  djhcvat42  41417  lcmineqlem4  42033  aks4d1p4  42080  aks4d1p5  42081  aks4d1p7  42084  aks4d1p8d2  42086  aks4d1p8  42088  hashnexinjle  42130  sticksstones1  42147  sticksstones2  42148  sticksstones10  42156  sticksstones12a  42158  aks6d1c7lem4  42184  aks6d1c7  42185  grpods  42195  unitscyglem2  42197  unitscyglem3  42198  unitscyglem4  42199  metakunt3  42208  metakunt4  42209  metakunt6  42211  metakunt7  42212  metakunt8  42213  metakunt10  42215  metakunt11  42216  metakunt12  42217  metakunt20  42225  metakunt21  42226  metakunt22  42227  metakunt30  42235  qsalrel  42281  supinf  42283  dvdsexpnn0  42369  redvmptabs  42390  sn-nnne0  42478  sn-sup2  42501  fimgmcyclem  42543  flt4lem2  42657  flt4lem7  42669  lzenom  42781  fphpdo  42828  irrapxlem4  42836  pellexlem6  42845  infmrgelbi  42889  pellfundre  42892  pellfundlb  42895  monotoddzz  42955  zindbi  42958  jm2.27  43020  rmydioph  43026  rpnnen3lem  43043  fnwe2lem2  43063  aomclem8  43073  hbtlem5  43140  hbt  43142  sdomne0  43426  sdomne0d  43427  ensucne0  43542  sucomisnotcard  43557  en2pr  43560  pr2cv  43561  refimssco  43620  rfovfvfvd  44016  rfovcnvf1od  44017  fsovrfovd  44022  nzss  44336  relprel  44972  wessf1ornlem  45190  axccdom  45227  dmrelrnrel  45231  axccd  45234  rnmptlb  45250  rnmptbdd  45252  rnmptbd2  45256  rnmptbdlem  45262  rnmptbd  45263  dstregt0  45293  suplesup  45350  supxrunb3  45410  supxrleubrnmpt  45417  rexabslelem  45429  rexabsle  45430  suprleubrnmpt  45433  infrnmptle  45434  infxrunb3rnmpt  45439  infxrpnf  45457  supminfxr  45475  infrpgernmpt  45476  xrpnf  45496  limsupre  45656  limsupref  45700  limsupbnd1f  45701  limsuppnfd  45717  climinf2  45722  limsuppnf  45726  climinfmpt  45730  climinf3  45731  limsupmnflem  45735  limsupmnf  45736  limsupre2  45740  limsupmnfuzlem  45741  limsupre2mpt  45745  limsupre3lem  45747  limsupre3  45748  limsupre3mpt  45749  limsupre3uzlem  45750  limsupre3uz  45751  limsupreuz  45752  limsupreuzmpt  45754  liminfval2  45783  liminfreuzlem  45817  liminfreuz  45818  xlimpnfxnegmnf  45829  cnrefiisplem  45844  xlimpnfv  45853  xlimpnf  45857  xlimpnfmpt  45859  dfxlim2  45863  icccncfext  45902  cncficcgt0  45903  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem5  46020  stoweidlem20  46035  stoweidlem26  46041  stoweidlem28  46043  stoweidlem29  46044  stoweidlem34  46049  wallispilem3  46082  stirlinglem13  46101  fourierdlem41  46163  fourierdlem42  46164  fourierdlem51  46172  fourierdlem54  46175  salunicl  46331  saluncl  46332  salexct  46349  salexct2  46354  salexct3  46357  salgencntex  46358  salgensscntex  46359  sge0pnffigt  46411  meadjuni  46472  omeunile  46520  ovnlerp  46577  hoidifhspval  46623  ovolval5lem2  46668  salpreimagelt  46722  pimincfltioo  46733  salpreimagtge  46740  salpreimagtlt  46745  incsmf  46757  issmfgt  46771  smfpreimagt  46777  decsmf  46782  issmfge  46785  smfpimgtxr  46795  smfpreimage  46797  smfinflem  46832  smfinf  46833  finfdm  46861  funressnfv  47055  funressnvmo  47057  funressnmo  47058  dfdfat2  47140  tz6.12-afv  47185  funressndmafv2rn  47235  tz6.12-afv2  47252  dfatcolem  47267  dfatco  47268  zplusmodne  47345  m1modne  47350  minusmod5ne  47351  submodneaddmod  47353  iccpartigtl  47410  iccpartgt  47414  icceuelpartlem  47422  iccpartnel  47425  sprsymrelfolem2  47480  goldbachthlem2  47533  odz2prm2pw  47550  fmtnoprmfac1  47552  fmtnoprmfac2  47554  fmtnofac2  47556  fmtno4prmfac  47559  fmtno4prm  47562  prmdvdsfmtnof1lem1  47571  31prm  47584  perfectALTVlem2  47709  nnsum3primes4  47775  nnsum3primesprm  47777  nnsum3primesgbe  47779  nnsum3primesle9  47781  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgblthelfgott  47802  tgoldbach  47804  gpg3nbgrvtxlem  48023  assintop  48125  isassintop  48126  assintopcllaw  48128  ztprmneprm  48263  ply1mulgsumlem1  48303  ply1mulgsumlem2  48304  lco0  48344  lcoel0  48345  lincsumcl  48348  lincscmcl  48349  lcoss  48353  linindslinci  48365  lindslinindsimp1  48374  linds0  48382  el0ldep  48383  lindsrng01  48385  ldepspr  48390  islindeps2  48400  isldepslvec2  48402  zlmodzxzldep  48421  ldepsnlinc  48425  elbigo2r  48474  tposres0  48777  lubsscl  48857  glbsscl  48858  lubprlem  48859  ipolub  48877  ipoglb  48880  catprslem  48899  setrec2lem1  49212