Theorem breq1 5111

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

Assertion

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

Proof of Theorem breq1

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  ⟨cop 4594   class class class wbr 5108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is referenced by:  breq12  5113  breq1i  5115  breq1d  5118  nbrne2  5130  brab1  5158  pocl  5577  swopolem  5579  swopo  5580  po2ne  5585  solin  5596  sotrieq  5600  sotr2  5603  isso2i  5606  somo  5608  dffr2  5622  frc  5624  frirr  5637  fr2nr  5638  wereu2  5658  vtoclr  5724  frsn  5749  brcog  5852  brcogw  5854  brcnvg  5865  dfdmf  5886  eldmg  5888  dmun  5900  dm0rn0  5914  dfrnf  5940  dmcosseq  5968  dmcosseqOLD  5969  dfres2  6043  imasng  6086  cotrg  6111  cnvsym  6114  asymref2  6117  sotri2  6129  somin1  6133  rnco  6253  coi1  6264  predtrss  6323  frpomin  6341  dffun2  6546  dffun6f  6551  funmo  6552  fun11  6610  fveq2  6881  eliman0  6918  nfunsn  6920  dffv2  6976  fvopab5  7023  dff3  7095  f1ompt  7106  fmptco  7125  dff13  7252  foeqcnvco  7298  isorel  7324  soisores  7325  soisoi  7326  isocnv  7328  isotr  7334  isomin  7335  isoini  7336  isopolem  7343  isosolem  7345  f1oiso  7349  f1oiso2  7350  weniso  7352  eqfunresadj  7358  caovordig  7615  caovordg  7617  caovord3d  7620  caovord  7621  caovord3  7623  caofrss  7713  caoftrn  7715  fr3nr  7770  dfwe2  7772  f1oweALT  7968  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  8709  ecopovsym  8816  ecopovtrn  8817  isfi  8971  en0  9014  en0ALT  9015  en1  9020  endisj  9051  xpcomco  9054  sbth  9084  2pwne  9120  disjenex  9122  ssenen  9138  findcard  9147  findcard2  9148  pssnn  9152  sbthfi  9182  nneneq  9189  php  9190  onomeneq  9197  sdom1  9209  1sdom2dom  9213  isinf  9224  fineqvlem  9225  en1eqsnbi  9235  findcard3  9242  frfi  9244  fiint  9285  mapfienlem1  9364  mapfienlem2  9365  mapfienlem3  9366  mapfien  9367  marypha1lem  9392  supmo  9411  eqsup  9415  supub  9418  suplub  9419  suppr  9431  supisolem  9433  supisoex  9434  infmin  9455  infmo  9456  fiinfg  9460  fiinf2g  9461  infpr  9464  ordtypecbv  9478  ordtypelem3  9481  ordtypelem6  9484  ordtypelem7  9485  ordtypelem9  9487  ordtypelem10  9488  hartogslem1  9503  hartogs  9505  wemaplem1  9507  wemaplem2  9508  wemapso2lem  9513  card2on  9515  card2inf  9516  elharval  9522  brwdom2  9534  wdomtr  9536  cantnfs  9634  cantnfp1lem2  9647  oemapso  9650  cantnflem1  9657  wemapwe  9665  ttrclss  9688  r111  9746  kardex  9879  karden  9880  isnumi  9931  tskwe  9935  cardid2  9938  cardonle  9942  cardne  9950  iscard2  9961  infxpenlem  9996  fodomfi2  10043  wdomfil  10044  wdomnumr  10047  alephsuc2  10063  infenaleph  10074  iunfictbso  10097  infpss  10198  cff1  10241  cfslb2n  10251  sornom  10260  fin4i  10281  isfin6  10283  isfin7  10284  isfin1-3  10369  fin1a2lem9  10391  fin1a2lem11  10393  hsmexlem4  10412  axcc2lem  10419  axcc4dom  10424  domtriomlem  10425  numthcor  10477  zorn2lem2  10480  zorn2lem3  10481  zorn2lem7  10485  zorn2g  10486  axdclem  10502  axdc  10504  brdom7disj  10514  brdom6disj  10515  uniimadom  10527  ondomon  10546  alephval2  10556  alephreg  10566  pwcfsdom  10567  elgch  10606  gchi  10608  fpwwe2lem11  10625  fpwwe2lem12  10626  winainflem  10677  winalim2  10680  tsken  10738  0tsk  10739  inar1  10759  tskord  10764  tskuni  10767  grudomon  10801  pinq  10911  nqereu  10913  enqeq  10918  ltbtwnnq  10962  ltrnq  10963  prcdnq  10977  prnmax  10979  genpnmax  10991  nqpr  10998  1idpr  11013  reclem2pr  11032  reclem3pr  11033  reclem4pr  11034  recexpr  11035  supexpr  11038  ltsosr  11078  1ne0sr  11080  ltasr  11084  supsrlem  11095  axpre-lttri  11149  axpre-lttrn  11150  axpre-ltadd  11151  axpre-sup  11153  lelttr  11299  dedekind  11372  dedekindle  11373  ltordlem  11738  lt0ne0d  11778  fimaxre3  12160  fiminre2  12162  lbreu  12164  lble  12166  sup2  12170  infm3  12173  suprleub  12180  supaddc  12181  supadd  12182  supmul1  12183  supmullem1  12184  supmul  12186  nnne0  12269  nnsub  12279  nominpos  12480  nnunb  12499  arch  12500  nn0sub  12553  nn0n0n1ge2b  12572  nn0lt10b  12657  zextle  12668  peano5uzti  12685  fzind  12693  btwnz  12698  uzval  12863  uzwo  12934  nnwof  12937  ublbneg  12956  lbzbi  12959  zsupss  12960  uzsupss  12963  uzwo3  12966  zmax  12968  rebtwnz  12970  rpnnen1lem3  13002  xrltnsym  13161  xrlttri  13163  xrlttr  13164  xrlelttr  13180  nltpnft  13189  xrmaxlt  13206  xrmaxle  13208  qbtwnre  13224  qbtwnxr  13225  xltnegi  13241  xnn0lenn0nn0  13270  xsubge0  13286  xlesubadd  13288  xmullem2  13290  xlemul1a  13313  xrinfmexpnf  13331  xrsupsslem  13332  xrinfmsslem  13333  xrub  13337  supxrunb1  13344  supxrunb2  13345  reltre  13366  rpltrp  13367  reltxrnmnf  13368  ixxval  13379  elixx1  13380  elioo2  13412  iccid  13416  icc0  13419  fzval  13536  elfz1  13539  elfznelfzo  13801  elfznelfzob  13802  flval  13826  fllelt  13829  flflp1  13839  flval2  13846  flval3  13847  flbi  13848  dfceil2  13871  ceilval2  13872  fleqceilz  13886  modid2  13930  addmodlteq  13981  fsequb2  14011  ssnn0fi  14020  seqf1olem2  14077  sqlecan  14244  faclbnd4lem1  14328  hashsnle1  14453  pr2pwpr  14515  hash3tpde  14529  rtrclreclem3  15096  relexpindlem  15099  sgnval  15124  sgnmulsgn  15145  01sqrexlem6  15297  01sqrex  15299  abslt  15365  absle  15366  rexanre  15397  rexico  15404  limsupgle  15527  limsupgre  15531  limsupbnd2  15533  rlim2lt  15547  rlim3  15548  ello12r  15567  ello1d  15573  elo12r  15578  rlimconst  15594  climshft  15626  rlimcn3  15640  o1rlimmul  15669  lo1le  15702  climsup  15720  caucvgrlem  15723  isumless  15898  divrcnv  15905  cvgrat  15936  rpnnen2lem10  16278  ruclem1  16286  ruclem2  16287  ruclem11  16295  ruclem12  16296  sqrt2irr  16304  absdvdsb  16331  dvdsle  16367  dvdsabseq  16370  dvdsdivcl  16373  dvdsext  16378  divalglem8  16457  divalglem9  16458  divalglem10  16459  divalgmod  16463  ndvdssub  16466  sadcaddlem  16514  gcdcllem1  16556  gcdcllem2  16557  gcdcllem3  16558  dfgcd2  16603  gcdzeq  16609  dvdssq  16624  nn0seqcvgd  16627  algcvgblem  16634  lcmval  16649  lcmdvds  16665  lcmgcdeq  16669  lcmfpr  16684  lcmf  16690  lcmftp  16693  lcmfunsnlem1  16694  lcmfunsnlem2lem1  16695  lcmfunsnlem2lem2  16696  lcmfdvdsb  16700  coprmgcdb  16706  coprmdvds1  16709  1nprm  16736  1idssfct  16737  isprm2lem  16738  isprm2  16739  dvdsprime  16744  nprm  16745  3prm  16751  dvdsprm  16761  exprmfct  16762  isprm5  16765  maxprmfct  16767  coprm  16769  prmdvdsncoprmbd  16785  ncoprmlnprm  16786  eulerthlem2  16840  phisum  16849  odzval  16850  pythagtriplem4  16878  pc2dvds  16938  pcprmpw2  16941  pcprmpw  16942  dvdsprmpweqle  16945  oddprmdvds  16962  prmpwdvds  16963  pockthg  16965  unbenlem  16967  prmreclem4  16978  prmreclem5  16979  prmreclem6  16980  1arith  16986  vdwlem6  17045  vdwlem11  17050  vdwlem13  17052  ramtlecl  17059  ramub  17072  rami  17074  ramubcl  17077  0ram  17079  ram0  17081  prmdvdsprmop  17102  prmolefac  17105  prmodvdslcmf  17106  prmgaplem2  17109  prmgaplcmlem1  17110  prmgaplcmlem2  17111  prmgaplem3  17112  prmgaplem4  17113  prmgaplem5  17114  prmgaplem6  17115  prmgapprmolem  17120  prmlem0  17164  prmlem1a  17165  imasaddfnlem  17581  imasvscafn  17590  imasleval  17594  prslem  18352  drsdir  18357  drsdirfi  18360  isdrs2  18361  posi  18372  posasymb  18374  pospropd  18380  pltval3  18392  plelttr  18397  pospo  18398  lubprop  18411  luble  18412  lublecllem  18413  glbprop  18424  joinval2lem  18433  joinlem  18436  meetlem  18450  meetle  18453  poslubmo  18464  posglbmo  18465  poslubd  18466  tleile  18474  latnlej  18511  isglbd  18564  lubub  18566  lubun  18570  clatleglb  18573  tsrlin  18640  letsr  18648  dirge  18658  pmtrval  19520  pmtrrn  19526  pmtrfrn  19527  pmtrrn2  19529  pmtrsn  19588  mndodcongi  19612  odeq  19619  odmulgeq  19626  gexnnod  19657  sylow1lem1  19667  pgpssslw  19683  sylow2a  19688  efgredeu  19821  efgred2  19822  gexex  19922  frgpnabllem2  19943  cyggenod  19953  dprdval  20074  dprdw  20081  dprdwd  20082  ablfacrplem  20136  ablfac1c  20142  ablfac1eu  20144  ablfaclem3  20158  omndadd  20197  abvtrivd  20914  zringlpir  21596  prmirredlem  21601  znleval  21683  frlmelbas  21885  ellspd  21931  islindf4  21967  psrbagconcl  22056  psrbagleadd1  22057  gsumbagdiaglem  22060  rhmpsrlem2  22070  psrlidm  22090  psrridm  22091  psrass1  22092  psrcom  22096  mplelbas  22119  mplmonmul  22166  ltbwe  22174  mhpmulcl  22291  psdmul  22308  coe1fsupp  22353  coe1ae0  22355  coe1mul2  22409  coe1tmmul  22417  pmatcoe1fsupp  22837  chfacffsupp  22992  chfacfscmulfsupp  22995  chfacfscmulgsum  22996  chfacfpmmulfsupp  22999  chfacfpmmulgsum  23000  ordtbas2  23327  ordtopn2  23331  ordtrest2lem  23339  pnfnei  23356  ordtt1  23515  ordthauslem  23519  2ndci  23584  2ndcsb  23585  2ndcredom  23586  2ndc1stc  23587  1stcrest  23589  2ndcctbss  23591  2ndcdisj  23592  2ndcsep  23595  lly1stc  23632  tx1stc  23786  ordthmeolem  23937  ufildom1  24062  xmetrtri2  24492  prdsxmetlem  24504  ssblex  24564  prdsbl  24627  comet  24649  stdbdxmet  24651  stdbdmopn  24654  met1stc  24657  dscmet  24708  metdstri  24988  metdscn  24993  xrhmeo  25084  bndth  25096  evth  25097  lebnumlem3  25101  pcovalg  25150  pco1  25153  pcocn  25155  pcopt  25160  pcopt2  25161  pcoass  25162  nmoleub3  25257  bcthlem5  25466  rrxfsupp  25540  minveclem4c  25563  minveclem2  25564  minveclem3b  25566  minveclem4  25570  minveclem6  25572  pmltpclem1  25586  pmltpc  25588  ovollb2lem  25626  ovolctb  25628  ovolunlem1  25635  ovoliunlem1  25640  ovoliunlem2  25641  ovoliun2  25644  ovolshftlem1  25647  ovolscalem1  25651  ovolicc1  25654  ovolicc2lem3  25657  voliunlem2  25689  voliunlem3  25690  ioombl1lem4  25699  uniioovol  25717  uniioombllem2  25721  uniioombllem3  25723  uniioombllem6  25726  volsup2  25743  ismbfd  25777  mbfsup  25802  mbflimsup  25804  itg1climres  25852  mbfi1fseqlem4  25856  itg2lr  25868  itg2leub  25872  itg2seq  25880  itg2monolem1  25888  itg2monolem3  25890  itg2mono  25891  itg2i1fseq2  25894  itg2gt0  25898  itg2cnlem1  25899  itg2cnlem2  25900  itg2cn  25901  iblss  25943  itgless  25955  ibladdlem  25958  iblabsr  25968  iblmulc2  25969  itgabs  25973  bddiblnc  25980  ditgeq1  25986  dvferm2lem  26124  rolle  26128  dvlip2  26133  c1liplem1  26134  c1lip1  26135  dvfsumlem2  26165  dvfsumlem4  26167  mdegleb  26200  degltlem1  26208  plyco0  26328  plyeq0lem  26346  coeeq2  26378  dgrle  26379  dgradd2  26404  plydiveu  26438  aareccl  26466  aalioulem2  26473  aaliou3lem7  26489  psercnlem1  26564  pilem2  26591  pilem3  26592  logltb  26741  divlogrlim  26776  logcnlem3  26785  cxpaddlelem  26892  rlimcnp  27106  cxplim  27112  cxploglim  27118  scvxcvx  27126  ftalem1  27213  ftalem2  27214  isppw2  27255  vmappw  27256  sgmnncl  27287  sqff1o  27322  fsumdvdsdiaglem  27323  dvdsppwf1o  27326  dvdsflsumcom  27328  musum  27331  muinv  27333  mpodvdsmulf1o  27334  dvdsmulf1o  27336  vmalelog  27345  vmasum  27356  logfac2  27357  perfectlem2  27370  bcmono  27417  bpos1lem  27422  bposlem9  27432  lgsmod  27463  lgsne0  27475  gausslemma2dlem4  27509  2sqlem6  27563  2sqlem8  27566  2sqlem10  27568  2sqreulem1  27586  2sqreunnlem1  27589  chtppilim  27615  rpvmasumlem  27627  dchrisumlema  27628  dchrisumlem2  27630  dchrvmasumlem1  27635  dchrvmasumiflem1  27641  dchrisum0flblem1  27648  dchrisum0flblem2  27649  dchrisum0  27660  rplogsum  27667  logsqvma  27682  pntpbnd1  27726  pntpbnd2  27727  pntibndlem3  27732  pntlemj  27743  pntlemi  27744  pntlem3  27749  pnt3  27752  ostth3  27778  nodense  27832  noresle  27837  nosupprefixmo  27840  noinfprefixmo  27841  nosupcbv  27842  nosupdm  27844  nosupbnd1lem1  27848  nosupbnd1lem4  27851  nosupbnd1  27854  nosupbnd2lem1  27855  nosupbnd2  27856  noinfcbv  27857  noinfdm  27859  noinffv  27861  noinfres  27862  noinfbnd1lem3  27865  noinfbnd1lem4  27866  noinfbnd1lem5  27867  noinfbnd1  27869  noetalem2  27882  nocvxminlem  27923  sltssnb  27938  sltssepc  27940  conway  27948  cutsval  27949  etaslts  27962  lesrec  27968  eqcuts3  27973  bday1  27983  cuteq1  27986  madeval2  28002  rightval  28019  elleft  28020  sltsright  28030  made0  28032  madecut  28052  left1s  28064  madebdaylemlrcut  28068  ltslpss  28077  cofslts  28087  coinitslts  28088  cofcutr  28093  cofcutrtime  28096  cofss  28099  coiniss  28100  cutmax  28103  cutmin  28104  cutminmax  28105  addsproplem1  28138  addsprop  28145  leadds1  28158  addsuniflem  28170  negsproplem1  28197  negsprop  28204  negsid  28210  negsunif  28224  mulsproplemcbv  28284  mulsproplem1  28285  mulsproplem9  28293  mulsprop  28299  sltmuls1  28316  sltmuls2  28317  mulsuniflem  28318  precsexlem11  28386  abslts  28418  oncutlt  28433  oniso  28440  bdayons  28445  addonbday  28448  n0fincut  28524  onsfi  28525  n0subs  28532  bdayn0p1  28538  eucliddivs  28545  zcuts  28576  twocut  28592  halfcut  28627  addhalfcut  28628  bdaypw2n0bndlem  28632  bdayfinbndcbv  28635  bdayfinbndlem1  28636  bdayfinbndlem2  28637  z12bdaylem1  28639  elreno  28660  elreno2  28664  tgjustc1  28720  tgjustc2  28721  iscgrglt  28759  tgcgr4  28776  hlcgreu  28866  elplng  29036  plngcplem  29041  lmif  29068  islmib  29070  trgcopyeu  29090  iscgrad  29095  inaghl  29135  axlowdim2  29276  axlowdim  29277  axcontlem2  29281  axcontlem3  29282  axcontlem4  29283  axcontlem7  29286  axcontlem9  29288  axcontlem10  29289  axcontlem11  29290  axcontlem12  29291  ebtwntg  29298  umgrupgr  29419  nbusgrvtxm1  29695  crctcshwlkn0lem2  30126  crctcshwlkn0lem3  30127  crctcsh  30139  wlkswwlksf1o  30194  clwlkclwwlklem2fv1  30312  clwlkclwwlkf  30325  0clwlkv  30448  eupth2  30556  numclwwlk5  30705  nmoubi  31090  minvecolem2  31193  minvecolem3  31194  minvecolem4c  31197  minvecolem4  31198  minvecolem5  31199  minvecolem6  31200  htthlem  31235  chlimi  31552  chcompl  31560  hsn0elch  31566  cmbr3  31926  cmcm  31932  cmcm3  31933  lecm  31935  nmopub  32226  nmfnleub  32243  nmopun  32332  nmcexi  32344  cnlnadjlem7  32391  pjnmopi  32466  stle0i  32557  stlesi  32559  stm1i  32561  csmdsymi  32652  cvmd  32654  atcveq0  32666  atcv1  32698  atord  32706  atcvat2  32707  chirred  32713  mdsym  32730  mddmdin0i  32749  cdj1i  32751  fmptcof2  32968  fnpreimac  32981  isoun  33013  fcobijfs  33032  fcobijfs2  33033  lt2addrd  33061  xlt2addrd  33070  xrge0infss  33071  infxrge0glb  33076  xrofsup  33078  fz1nnct  33112  toslublem  33258  tosglblem  33260  ismntd  33270  mgccole1  33276  mgccole2  33277  mgcmnt1  33278  mgcmnt2  33279  dfmgc2lem  33281  dfmgc2  33282  psgnfzto1stlem  33386  fzto1st  33389  psgnfzto1st  33391  trsp2cyc  33409  xrnarchi  33470  archirng  33474  archiexdiv  33476  archiabl  33484  isarchiofld  33485  elrgspnlem1  33528  elrgspnlem2  33529  elrgspnlem3  33530  elrgspnlem4  33531  elrgspn  33532  elrgspnsubrunlem1  33533  elrgspnsubrunlem2  33534  elrgspnsubrun  33535  linds2eq  33660  elrspunidl  33702  elrspunsn  33703  isrprm  33773  evl1deg1  33832  evl1deg2  33833  evl1deg3  33834  0mplrim  33870  selvply1rhmlema  33874  selvply1rhmlemb  33875  selvply1rhmlem1  33876  selvply1rhmlem2  33877  selvply1rhmlem4  33879  selvply1rhm0  33882  extvfvvcl  33891  extvfvcl  33892  mplmulmvr  33895  evlextv  33898  mplvrpmlem  33899  mplvrpmfgalem  33900  mplvrpmga  33901  mplvrpmmhm  33902  mplvrpmrhm  33903  psrmonmul  33906  psrmonprod  33908  esplyfval0  33920  esplylem  33922  esplyfv1  33925  esplyfval3  33928  esplyfvaln  33930  esplyind  33931  ply1degltdimlem  33978  lbsdiflsp0  33982  fedgmullem1  33985  fedgmullem2  33986  fedgmul  33987  fldextrspunlsplem  34029  fldextrspunlsp  34030  smatrcl  34152  smatlem  34153  madjusmdetlem2  34184  madjusmdet  34187  cmpcref  34206  ldlfcntref  34210  dispcmp  34215  zarcmplem  34237  ordtrest2NEWlem  34278  ordtconnlem1  34280  xrge0iifiso  34291  rge0scvg  34305  gsumesum  34415  esumfsup  34426  esumpinfval  34429  esumpcvgval  34434  esumcvg  34442  sigaclcu  34473  sigaclci  34488  unelsiga  34490  unelldsys  34514  sigapildsys  34518  ldgenpisyslem1  34519  fiunelros  34530  measvun  34565  voliune  34585  volfiniune  34586  oms0  34653  omssubaddlem  34655  omssubadd  34656  carsgsigalem  34671  carsgclctunlem2  34675  carsgclctun  34677  pmeasmono  34680  pmeasadd  34681  orvcval2  34815  dstfrvel  34830  ballotlemfc0  34849  ballotlemfcc  34850  ballotlemsv  34866  ballotlemsf1o  34870  breprexp  34986  tgoldbachgt  35016  bnj23  35073  bnj1185  35147  bnj1152  35352  bnj1418  35394  fnrelpredd  35446  kardval2  35520  elkarden  35522  kardeng  35524  kardnnfi  35536  rankkardu  35538  loop1cycl  35583  umgr2cycl  35587  acycgrcycl  35593  dfdm5  36219  dfrn5  36220  wzel  36268  wsuclem  36269  brpprod  36329  brsset  36333  brbigcup  36342  dffix2  36349  elfuns  36359  brimageg  36371  brdomaing  36379  brrangeg  36380  brimg  36381  brapply  36382  lemsuccf  36385  funpartlem  36388  brrestrict  36395  dfrecs2  36396  dfrdg4  36397  brofs  36451  btwncomim  36459  btwnintr  36465  btwnexch3  36466  btwnexch2  36469  brifs  36489  brcolinear2  36504  colineardim1  36507  brfs  36525  btwnconn1  36547  segcon2  36551  seglerflx  36558  seglemin  36559  btwnsegle  36563  colinbtwnle  36564  broutsideof2  36568  fvray  36587  lineunray  36593  lineelsb2  36594  linerflx1  36595  trer  36771  elicc3  36772  finminlem  36773  nn0prpwlem  36777  nn0prpw  36778  fnessref  36812  refssfne  36813  weiunlem  36918  weiunfrlem  36919  weiunfr  36922  weiunse  36923  unblimceq0lem  37039  unblimceq0  37040  unbdqndv2  37044  knoppndvlem21  37065  taupilemrplb  37908  dfgcd3  37912  icorempo  37941  icoreval  37943  iooelexlt  37952  relowlssretop  37953  domalom  37994  ctbssinf  37996  pibt2  38007  phpreu  38199  fin2solem  38201  fin2so  38202  ltflcei  38203  ptrecube  38215  poimirlem1  38216  poimirlem2  38217  poimirlem5  38220  poimirlem6  38221  poimirlem7  38222  poimirlem9  38224  poimirlem12  38227  poimirlem22  38237  poimirlem23  38238  poimirlem24  38239  poimirlem26  38241  poimirlem27  38242  poimirlem32  38247  heicant  38250  mblfinlem1  38252  mblfinlem2  38253  itg2addnclem  38266  itg2addnclem3  38268  itg2addnc  38269  itg2gt0cn  38270  ibladdnclem  38271  iblmulc2nc  38280  itgabsnc  38284  ftc1anclem5  38292  ftc1anclem7  38294  ftc1anclem8  38295  ftc1anc  38296  indexdom  38329  filbcmb  38335  fdc  38340  prdsbnd  38388  heiborlem3  38408  rrnequiv  38430  rngoueqz  38535  eqbrtr  38833  elrnressn  38875  inxprnres  38893  presucmap  39090  eqvreltr  39286  prtlem10  39585  lsatcveq0  39752  lsatcv1  39768  oposlem  39902  opnlen0  39908  lub0N  39909  glb0N  39913  omllaw  39963  cmtbr4N  39975  cvrval  39989  cvrnbtwn  39991  cvrnbtwn2  39995  cvrnbtwn3  39996  cvrcon3b  39997  cvrnbtwn4  39999  atcvreq0  40034  atnle  40037  atlatmstc  40039  cvlexch1  40048  glbconN  40097  hlsuprexch  40101  exatleN  40124  cvratlem  40141  atcvrj0  40148  atcvrj2b  40152  atlelt  40158  cvrat4  40163  3dim1lem5  40186  3dim2  40188  3dim3  40189  ps-2  40198  llni  40228  llnn0  40236  llnle  40238  lplni  40252  lplni2  40257  lplnle  40260  lplnn0N  40267  llncvrlpln  40278  2llnjN  40287  lvoli  40295  lvoli3  40297  lvoli2  40301  lvoln0N  40311  4at  40333  lplncvrlvol  40336  2lplnj  40340  dalemcea  40380  dalem3  40384  psubspi  40467  linepsubN  40472  elpmap  40478  pmapsub  40488  lnatexN  40499  cdlema1N  40511  cdlemb  40514  elpadd  40519  paddvaln0N  40521  paddasslem5  40544  llnexchb2lem  40588  llnexch2N  40590  islhp  40716  lhpat3  40766  4atexlemex2  40791  4atex  40796  4atex2-0aOLDN  40798  4atex2-0cOLDN  40800  lautle  40804  lautcvr  40812  lauteq  40815  ldilval  40833  ltrnu  40841  trlval2  40883  trlne  40905  cdleme0ex1N  40943  cdleme0nex  41010  cdleme18d  41015  cdlemednuN  41020  cdleme25b  41074  cdleme25cv  41078  cdleme27b  41088  cdleme29b  41095  cdleme31sn  41100  cdleme31fv  41110  cdleme31fv2  41113  cdlemefrs29bpre0  41116  cdlemefr29bpre0N  41126  cdlemefr29clN  41127  cdlemefr32fvaN  41129  cdlemefr32fva1  41130  cdlemefs29pre00N  41132  cdlemefs32sn1aw  41134  cdlemefs29bpre0N  41136  cdlemefs29bpre1N  41137  cdlemefs29cpre1N  41138  cdlemefs29clN  41139  cdlemefs32fvaN  41142  cdlemefs32fva1  41143  cdleme41sn3a  41153  cdleme32fva  41157  cdleme32e  41165  cdleme35f  41174  cdleme40v  41189  cdleme42b  41198  trlord  41289  cdlemg1cex  41308  diaval  41752  diaeldm  41756  diaelrnN  41765  cdlemm10N  41838  dibglbN  41886  dicval  41896  dicfnN  41903  dicvalrelN  41905  dihval  41952  dihlsscpre  41954  dihglblem3N  42015  dihmeetlem2N  42019  djhcvat42  42135  lcmineqlem4  42745  aks4d1p4  42792  aks4d1p5  42793  aks4d1p7  42796  aks4d1p8d2  42798  aks4d1p8  42800  hashnexinjle  42842  sticksstones1  42859  sticksstones2  42860  sticksstones10  42868  sticksstones12a  42870  aks6d1c7lem4  42896  aks6d1c7  42897  grpods  42907  unitscyglem2  42909  unitscyglem3  42910  unitscyglem4  42911  qsalrel  42955  supinf  42956  dvdsexpnn0  43041  redvmptabs  43067  sn-nnne0  43180  sn-sup2  43211  fimgmcyclem  43249  flt4lem2  43327  flt4lem7  43339  lzenom  43449  fphpdo  43492  irrapxlem4  43500  pellexlem6  43509  infmrgelbi  43553  pellfundre  43556  pellfundlb  43559  monotoddzz  43618  zindbi  43621  jm2.27  43683  rmydioph  43689  rpnnen3lem  43706  fnwe2lem2  43726  aomclem8  43736  hbtlem5  43803  hbt  43805  sdomne0  44087  sdomne0d  44088  ensucne0  44203  sucomisnotcard  44218  en2pr  44221  pr2cv  44222  refimssco  44281  rfovfvfvd  44677  rfovcnvf1od  44678  fsovrfovd  44683  nzss  44975  relprel  45608  permaxinf2lem  45669  wessf1ornlem  45851  axccdom  45886  dmrelrnrel  45890  axccd  45892  rnmptlb  45906  rnmptbdd  45908  rnmptbd2  45912  rnmptbdlem  45918  rnmptbd  45919  dstregt0  45949  suplesup  46003  supxrunb3  46062  supxrleubrnmpt  46068  rexabslelem  46080  rexabsle  46081  suprleubrnmpt  46084  infrnmptle  46085  infxrunb3rnmpt  46090  infxrpnf  46108  supminfxr  46126  infrpgernmpt  46127  xrpnf  46147  limsupre  46303  limsupref  46347  limsupbnd1f  46348  limsuppnfd  46364  climinf2  46369  limsuppnf  46373  climinfmpt  46377  climinf3  46378  limsupmnflem  46382  limsupmnf  46383  limsupre2  46387  limsupmnfuzlem  46388  limsupre2mpt  46392  limsupre3lem  46394  limsupre3  46395  limsupre3mpt  46396  limsupre3uzlem  46397  limsupre3uz  46398  limsupreuz  46399  limsupreuzmpt  46401  liminfval2  46430  liminfreuzlem  46464  liminfreuz  46465  xlimpnfxnegmnf  46476  cnrefiisplem  46491  xlimpnfv  46500  xlimpnf  46504  xlimpnfmpt  46506  dfxlim2  46510  icccncfext  46549  cncficcgt0  46550  ioodvbdlimc1lem2  46594  ioodvbdlimc2lem  46596  stoweidlem5  46667  stoweidlem20  46682  stoweidlem26  46688  stoweidlem28  46690  stoweidlem29  46691  stoweidlem34  46696  wallispilem3  46729  stirlinglem13  46748  fourierdlem41  46810  fourierdlem42  46811  fourierdlem51  46819  fourierdlem54  46822  salunicl  46978  saluncl  46979  salexct  46996  salexct2  47001  salexct3  47004  salgencntex  47005  salgensscntex  47006  sge0pnffigt  47058  meadjuni  47119  omeunile  47167  ovnlerp  47224  hoidifhspval  47270  ovolval5lem2  47315  salpreimagelt  47369  pimincfltioo  47380  salpreimagtge  47387  salpreimagtlt  47392  incsmf  47404  issmfgt  47418  smfpreimagt  47424  decsmf  47429  issmfge  47432  smfpimgtxr  47442  smfpreimage  47444  smfinflem  47479  smfinf  47480  finfdm  47508  funressnfv  47725  funressnvmo  47727  funressnmo  47728  dfdfat2  47810  tz6.12-afv  47855  funressndmafv2rn  47905  tz6.12-afv2  47922  dfatcolem  47937  dfatco  47938  zplusmodne  48031  m1modne  48036  minusmod5ne  48037  submodneaddmod  48039  modmknepk  48050  iccpartigtl  48117  iccpartgt  48121  icceuelpartlem  48129  iccpartnel  48132  sprsymrelfolem2  48187  nprmmul2  48222  goldbachthlem2  48243  odz2prm2pw  48260  fmtnoprmfac1  48262  fmtnoprmfac2  48264  fmtnofac2  48266  fmtno4prmfac  48269  fmtno4prm  48272  prmdvdsfmtnof1lem1  48281  31prm  48294  nprmdvdsfacm1  48321  perfectALTVlem2  48432  nnsum3primes4  48498  nnsum3primesprm  48500  nnsum3primesgbe  48502  nnsum3primesle9  48504  nnsum4primeseven  48510  nnsum4primesevenALTV  48511  wtgoldbnnsum4prm  48512  bgoldbnnsum3prm  48514  bgoldbtbndlem4  48518  bgoldbtbnd  48519  tgblthelfgott  48525  tgoldbach  48527  assintop  48919  isassintop  48920  assintopcllaw  48922  ztprmneprm  49072  ply1mulgsumlem1  49111  ply1mulgsumlem2  49112  lco0  49152  lcoel0  49153  lincsumcl  49156  lincscmcl  49157  lcoss  49161  linindslinci  49173  lindslinindsimp1  49182  linds0  49190  el0ldep  49191  lindsrng01  49193  ldepspr  49198  islindeps2  49208  isldepslvec2  49210  zlmodzxzldep  49229  ldepsnlinc  49233  elbigo2r  49278  xpco2  49580  tposres0  49600  lubsscl  49683  glbsscl  49684  lubprlem  49685  ipolub  49711  ipoglb  49714  catprslem  49733  infsubc2  49784  nelsubc3lem  49793  cnelsubclem  50326  setrec2lem1  50416