Theorem breq1 5105

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

Assertion

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

Proof of Theorem breq1

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  breq12  5107  breq1i  5109  breq1d  5112  nbrne2  5124  brab1  5152  pocl  5566  swopolem  5568  swopo  5569  po2ne  5574  solin  5585  sotrieq  5589  sotr2  5592  isso2i  5595  somo  5597  dffr2  5611  frc  5613  frirr  5626  fr2nr  5627  wereu2  5647  vtoclr  5713  frsn  5738  brcog  5843  brcogw  5845  brcnvg  5856  dfdmf  5877  eldmg  5879  dmun  5891  dm0rn0  5905  dfrnf  5931  dmcosseq  5959  dmcosseqOLD  5960  dfres2  6032  imasng  6081  cotrg  6104  cnvsym  6107  asymref2  6110  sotri2  6122  somin1  6126  rnco  6253  coi1  6264  predtrss  6325  frpomin  6343  dffun2  6548  dffun6f  6553  funmo  6554  fun11  6614  fveq2  6885  eliman0  6922  nfunsn  6924  dffv2  6980  fvopab5  7027  dff3  7100  f1ompt  7111  fmptco  7130  dff13  7258  foeqcnvco  7308  isorel  7334  soisores  7335  soisoi  7336  isocnv  7338  isotr  7344  isomin  7345  isoini  7346  isopolem  7353  isosolem  7355  f1oiso  7359  f1oiso2  7360  weniso  7364  eqfunresadj  7370  caovordig  7626  caovordg  7628  caovord3d  7631  caovord  7632  caovord3  7634  caofrss  7732  caoftrn  7734  fr3nr  7786  dfwe2  7788  f1oweALT  7984  frxp  8138  poxp  8140  fnwe2lem3  8147  fnse  8150  poxp2  8160  frxp2  8161  poxp3  8167  frxp3  8168  xpord3pred  8169  poseq  8175  brtpos2  8249  rntpos  8256  tpostpos  8263  frrlem12  8315  ertr  8733  ecopovsym  8840  ecopovtrn  8841  isfi  9002  en0  9045  en0ALT  9046  en1  9051  endisj  9083  xpcomco  9086  sbth  9116  2pwne  9152  disjenex  9154  ssenen  9170  findcard  9179  findcard2  9180  pssnn  9184  sbthfi  9214  nneneq  9221  php  9222  onomeneq  9229  sdom1  9241  1sdom2dom  9245  isinf  9256  fineqvlem  9257  en1eqsnbi  9267  findcard3  9274  frfi  9276  fiint  9318  mapfienlem1  9397  mapfienlem2  9398  mapfienlem3  9399  mapfien  9400  marypha1lem  9425  supmo  9444  eqsup  9448  supub  9451  suplub  9452  suppr  9464  supisolem  9466  supisoex  9467  infmin  9488  infmo  9489  fiinfg  9493  fiinf2g  9494  infpr  9497  ordtypecbv  9511  ordtypelem3  9514  ordtypelem6  9517  ordtypelem7  9518  ordtypelem9  9520  ordtypelem10  9521  hartogslem1  9536  hartogs  9538  wemaplem1  9540  wemaplem2  9541  wemapso2lem  9546  card2on  9548  card2inf  9549  elharval  9555  brwdom2  9567  wdomtr  9569  cantnfs  9667  cantnfp1lem2  9680  oemapso  9683  cantnflem1  9690  wemapwe  9698  ttrclss  9721  r111  9782  kardexOLD  9958  karden  9959  kardenOLD  9960  setrec2lem1  9974  isnumi  10027  tskwe  10031  cardid2  10034  cardonle  10038  cardne  10046  iscard2  10057  infxpenlem  10092  fodomfi2  10139  wdomfil  10140  wdomnumr  10143  alephsuc2  10159  infenaleph  10170  iunfictbso  10193  infpss  10294  cff1  10336  cfslb2n  10346  sornom  10355  fin4i  10376  isfin6  10378  isfin7  10379  isfin1-3  10464  fin1a2lem9  10486  fin1a2lem11  10488  hsmexlem4  10507  axcc2lem  10514  axcc4dom  10519  domtriomlem  10520  numthcor  10572  zorn2lem2  10575  zorn2lem3  10576  zorn2lem7  10580  zorn2g  10581  axdclem  10597  axdc  10599  brdom7disj  10610  brdom6disj  10611  uniimadom  10628  ondomon  10647  alephval2  10657  alephreg  10667  pwcfsdom  10668  elgch  10707  gchi  10709  fpwwe2lem11  10726  fpwwe2lem12  10727  winainflem  10778  winalim2  10781  tsken  10839  0tsk  10840  inar1  10860  tskord  10865  tskuni  10868  grudomon  10902  pinq  11012  nqereu  11014  enqeq  11019  ltbtwnnq  11063  ltrnq  11064  prcdnq  11078  prnmax  11080  genpnmax  11092  nqpr  11099  1idpr  11114  reclem2pr  11133  reclem3pr  11134  reclem4pr  11135  recexpr  11136  supexpr  11139  ltsosr  11179  1ne0sr  11181  ltasr  11185  supsrlem  11196  axpre-lttri  11250  axpre-lttrn  11251  axpre-ltadd  11252  axpre-sup  11254  lelttr  11400  dedekind  11473  dedekindle  11474  ltordlem  11841  lt0ne0d  11881  fimaxre3  12263  fiminre2  12265  lbreu  12267  lble  12269  sup2  12273  infm3  12276  suprleub  12283  supaddc  12284  supadd  12285  supmul1  12286  supmullem1  12287  supmul  12289  nnne0  12372  nnsub  12382  nominpos  12583  nnunb  12602  arch  12603  nn0sub  12656  nn0n0n1ge2b  12675  nn0lt10b  12761  zextle  12772  peano5uzti  12789  fzind  12797  btwnz  12802  uzval  12967  uzwo  13038  nnwof  13041  ublbneg  13060  lbzbi  13063  zsupss  13064  uzsupss  13067  uzwo3  13070  zmax  13072  rebtwnz  13074  rpnnen1lem3  13107  xrltnsym  13266  xrlttri  13268  xrlttr  13269  xrlelttr  13285  nltpnft  13294  xrmaxlt  13311  xrmaxle  13313  qbtwnre  13329  qbtwnxr  13330  xltnegi  13346  xnn0lenn0nn0  13375  xsubge0  13391  xlesubadd  13393  xmullem2  13395  xlemul1a  13418  xrinfmexpnf  13436  xrsupsslem  13437  xrinfmsslem  13438  xrub  13442  supxrunb1  13449  supxrunb2  13450  reltre  13471  rpltrp  13472  reltxrnmnf  13473  ixxval  13484  elixx1  13485  elioo2  13517  iccid  13521  icc0  13524  fzval  13641  elfz1  13644  elfznelfzo  13908  elfznelfzob  13909  flval  13934  fllelt  13937  flflp1  13947  flval2  13954  flval3  13955  flbi  13956  dfceil2  13979  ceilval2  13980  fleqceilz  13994  modid2  14038  addmodlteq  14089  fsequb2  14119  ssnn0fi  14128  seqf1olem2  14185  sqlecan  14353  faclbnd4lem1  14437  hashsnle1  14562  pr2pwpr  14624  hash3tpde  14638  rtrclreclem3  15213  relexpindlem  15216  sgnval  15241  sgnmulsgn  15262  01sqrexlem6  15414  01sqrex  15416  abslt  15482  absle  15483  rexanre  15514  rexico  15521  limsupgle  15644  limsupgre  15648  limsupbnd2  15650  rlim2lt  15664  rlim3  15665  ello12r  15684  ello1d  15690  elo12r  15695  rlimconst  15711  climshft  15743  rlimcn3  15757  o1rlimmul  15786  lo1le  15819  climsup  15837  caucvgrlem  15840  isumless  16014  divrcnv  16021  cvgrat  16052  rpnnen2lem10  16391  ruclem1  16399  ruclem2  16400  ruclem11  16408  ruclem12  16409  sqrt2irr  16417  absdvdsb  16444  dvdsle  16480  dvdsabseq  16483  dvdsdivcl  16486  dvdsext  16491  divalglem8  16570  divalglem9  16571  divalglem10  16572  divalgmod  16576  ndvdssub  16579  sadcaddlem  16627  gcdcllem1  16669  gcdcllem2  16670  gcdcllem3  16671  dfgcd2  16719  gcdzeq  16725  dvdssq  16742  nn0seqcvgd  16745  algcvgblem  16752  lcmval  16767  lcmdvds  16783  lcmgcdeq  16787  lcmfpr  16802  lcmf  16808  lcmftp  16811  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  lcmfdvdsb  16818  coprmgcdb  16824  coprmdvds1  16827  1nprm  16854  1idssfct  16855  isprm2lem  16856  isprm2  16857  dvdsprime  16862  nprm  16863  3prm  16869  dvdsprm  16879  exprmfct  16880  isprm5  16883  maxprmfct  16885  coprm  16887  prmdvdsncoprmbd  16903  ncoprmlnprm  16904  eulerthlem2  16959  phisum  16968  odzval  16969  pythagtriplem4  16997  pc2dvds  17057  pcprmpw2  17060  pcprmpw  17061  dvdsprmpweqle  17064  oddprmdvds  17081  prmpwdvds  17082  pockthg  17084  unbenlem  17086  prmreclem4  17097  prmreclem5  17098  prmreclem6  17099  1arith  17105  vdwlem6  17164  vdwlem11  17169  vdwlem13  17171  ramtlecl  17178  ramub  17191  rami  17193  ramubcl  17196  0ram  17198  ram0  17200  prmdvdsprmop  17221  prmolefac  17224  prmodvdslcmf  17225  prmgaplem2  17228  prmgaplcmlem1  17229  prmgaplcmlem2  17230  prmgaplem3  17231  prmgaplem4  17232  prmgaplem5  17233  prmgaplem6  17234  prmgapprmolem  17239  prmlem0  17283  prmlem1a  17284  imasaddfnlem  17700  imasvscafn  17709  imasleval  17713  prslem  18471  drsdir  18476  drsdirfi  18479  isdrs2  18480  posi  18491  posasymb  18493  pospropd  18499  pltval3  18511  plelttr  18516  pospo  18517  lubprop  18530  luble  18531  lublecllem  18532  glbprop  18543  joinval2lem  18552  joinlem  18555  meetlem  18569  meetle  18572  poslubmo  18583  posglbmo  18584  poslubd  18585  tleile  18593  latnlej  18630  isglbd  18683  lubub  18685  lubun  18689  clatleglb  18692  tsrlin  18759  letsr  18767  dirge  18777  pmtrval  19665  pmtrrn  19671  pmtrfrn  19672  pmtrrn2  19674  pmtrsn  19733  mndodcongi  19757  odeq  19764  odmulgeq  19771  gexnnod  19802  sylow1lem1  19812  pgpssslw  19828  sylow2a  19833  efgredeu  19966  efgred2  19967  gexex  20067  frgpnabllem2  20088  cyggenod  20098  dprdval  20219  dprdw  20226  dprdwd  20227  ablfacrplem  20281  ablfac1c  20287  ablfac1eu  20289  ablfaclem3  20303  omndadd  20342  abvtrivd  21089  zringlpir  21773  prmirredlem  21778  znleval  21860  frlmelbas  22062  ellspd  22108  islindf4  22144  psrbagconcl  22235  psrbagleadd1  22236  gsumbagdiaglem  22239  rhmpsrlem2  22249  psrlidm  22269  psrridm  22270  psrass1  22271  psrcom  22275  mplelbas  22298  mplmonmul  22345  ltbwe  22353  mhpmulcl  22470  psdmul  22487  coe1fsupp  22532  coe1ae0  22534  coe1mul2  22588  coe1tmmul  22596  pmatcoe1fsupp  23019  chfacffsupp  23174  chfacfscmulfsupp  23177  chfacfscmulgsum  23178  chfacfpmmulfsupp  23181  chfacfpmmulgsum  23182  ordtbas2  23509  ordtopn2  23513  ordtrest2lem  23521  pnfnei  23538  ordtt1  23697  ordthauslem  23701  2ndci  23766  2ndcsb  23767  2ndcredom  23768  2ndc1stc  23769  1stcrest  23771  2ndcctbss  23774  2ndcdisj  23775  2ndcsep  23778  lly1stc  23815  tx1stc  23969  ordthmeolem  24120  ufildom1  24245  xmetrtri2  24675  prdsxmetlem  24687  ssblex  24747  prdsbl  24810  comet  24832  stdbdxmet  24834  stdbdmopn  24837  met1stc  24840  dscmet  24891  metdstri  25171  metdscn  25176  xrhmeo  25267  bndth  25279  evth  25280  lebnumlem3  25284  pcovalg  25333  pco1  25336  pcocn  25338  pcopt  25343  pcopt2  25344  pcoass  25345  nmoleub3  25440  bcthlem5  25649  rrxfsupp  25723  minveclem4c  25746  minveclem2  25747  minveclem3b  25749  minveclem4  25753  minveclem6  25755  pmltpclem1  25769  pmltpc  25771  ovollb2lem  25809  ovolctb  25811  ovolunlem1  25818  ovoliunlem1  25823  ovoliunlem2  25824  ovoliun2  25827  ovolshftlem1  25830  ovolscalem1  25834  ovolicc1  25837  ovolicc2lem3  25840  voliunlem2  25872  voliunlem3  25873  ioombl1lem4  25882  uniioovol  25900  uniioombllem2  25904  uniioombllem3  25906  uniioombllem6  25909  volsup2  25926  ismbfd  25960  mbfsup  25985  mbflimsup  25987  itg1climres  26035  mbfi1fseqlem4  26039  itg2lr  26051  itg2leub  26055  itg2seq  26063  itg2monolem1  26071  itg2monolem3  26073  itg2mono  26074  itg2i1fseq2  26077  itg2gt0  26081  itg2cnlem1  26082  itg2cnlem2  26083  itg2cn  26084  iblss  26125  itgless  26137  ibladdlem  26140  iblabsr  26150  iblmulc2  26151  itgabs  26155  bddiblnc  26162  ditgeq1  26168  dvferm2lem  26306  rolle  26310  dvlip2  26315  c1liplem1  26316  c1lip1  26317  dvfsumlem2  26347  dvfsumlem4  26349  mdegleb  26382  degltlem1  26390  plyco0  26510  plyeq0lem  26529  coeeq2  26561  dgrle  26562  dgradd2  26587  plydiveu  26619  aareccl  26653  aalioulem2  26660  aaliou3lem7  26676  psercnlem1  26752  pilem2  26779  pilem3  26780  logltb  26928  divlogrlim  26963  logcnlem3  26972  cxpaddlelem  27079  rlimcnp  27293  cxplim  27299  cxploglim  27305  scvxcvx  27313  ftalem1  27400  ftalem2  27401  isppw2  27442  vmappw  27443  sgmnncl  27474  sqff1o  27509  fsumdvdsdiaglem  27510  dvdsppwf1o  27513  dvdsflsumcom  27515  musum  27518  muinv  27520  mpodvdsmulf1o  27521  dvdsmulf1o  27523  vmalelog  27532  vmasum  27543  logfac2  27544  perfectlem2  27557  bcmono  27604  bpos1lem  27609  bposlem9  27619  lgsmod  27650  lgsne0  27662  gausslemma2dlem4  27696  2sqlem6  27750  2sqlem8  27753  2sqlem10  27755  2sqreulem1  27773  2sqreunnlem1  27776  chtppilim  27802  rpvmasumlem  27814  dchrisumlema  27815  dchrisumlem2  27817  dchrvmasumlem1  27822  dchrvmasumiflem1  27828  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dchrisum0  27847  rplogsum  27854  logsqvma  27869  pntpbnd1  27913  pntpbnd2  27914  pntibndlem3  27919  pntlemj  27930  pntlemi  27931  pntlem3  27936  pnt3  27939  ostth3  27965  flt4lem2  27977  flt4lem7  27989  nodense  28049  noresle  28054  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupdm  28061  nosupbnd1lem1  28065  nosupbnd1lem4  28068  nosupbnd1  28071  nosupbnd2lem1  28072  nosupbnd2  28073  noinfcbv  28074  noinfdm  28076  noinffv  28078  noinfres  28079  noinfbnd1lem3  28082  noinfbnd1lem4  28083  noinfbnd1lem5  28084  noinfbnd1  28086  noetalem2  28099  nocvxminlem  28140  sltssnb  28155  sltssepc  28157  conway  28165  cutsval  28166  etaslts  28179  lesrec  28185  eqcuts3  28190  bday1  28200  cuteq1  28203  madeval2  28219  rightval  28236  elleft  28237  sltsright  28247  made0  28249  madecut  28269  left1s  28281  madebdaylemlrcut  28285  ltslpss  28294  cofslts  28304  coinitslts  28305  cofcutr  28310  cofcutrtime  28313  cofss  28316  coiniss  28317  cutmax  28320  cutmin  28321  cutminmax  28322  addsproplem1  28355  addsprop  28362  leadds1  28375  addsuniflem  28387  negsproplem1  28414  negsprop  28421  negsid  28427  negsunif  28441  mulsproplemcbv  28501  mulsproplem1  28502  mulsproplem9  28510  mulsprop  28516  sltmuls1  28533  sltmuls2  28534  mulsuniflem  28535  precsexlem11  28603  abslts  28635  oncutlt  28650  oniso  28657  bdayons  28662  addonbday  28665  n0fincut  28741  onsfi  28742  n0subs  28749  bdayn0p1  28755  eucliddivs  28762  zcuts  28793  twocut  28809  halfcut  28844  addhalfcut  28845  bdaypw2n0bndlem  28849  bdayfinbndcbv  28852  bdayfinbndlem1  28853  bdayfinbndlem2  28854  z12bdaylem1  28856  elreno  28877  elreno2  28881  tgjustc1  28937  tgjustc2  28938  iscgrglt  28977  tgcgr4  28994  hlcgreu  29084  elplng  29258  plngcplem  29263  lmif  29290  islmib  29292  trgcopyeu  29313  iscgrad  29318  inaghl  29364  axlowdim2  29538  axlowdim  29539  axcontlem2  29543  axcontlem3  29544  axcontlem4  29545  axcontlem7  29548  axcontlem9  29550  axcontlem10  29551  axcontlem11  29552  axcontlem12  29553  ebtwntg  29560  umgrupgr  29681  nbusgrvtxm1  29960  crctcshwlkn0lem2  30400  crctcshwlkn0lem3  30401  crctcsh  30413  wlkswwlksf1o  30468  clwlkclwwlklem2fv1  30586  clwlkclwwlkf  30599  0clwlkv  30722  loop1cycl  30744  umgr2cycl  30747  acycgrcycl  30753  eupth2  30840  numclwwlk5  30989  nmoubi  31374  minvecolem2  31477  minvecolem3  31478  minvecolem4c  31481  minvecolem4  31482  minvecolem5  31483  minvecolem6  31484  htthlem  31519  chlimi  31836  chcompl  31844  hsn0elch  31850  cmbr3  32210  cmcm  32216  cmcm3  32217  lecm  32219  nmopub  32510  nmfnleub  32527  nmopun  32616  nmcexi  32628  cnlnadjlem7  32675  pjnmopi  32750  stle0i  32841  stlesi  32843  stm1i  32845  csmdsymi  32936  cvmd  32938  atcveq0  32950  atcv1  32982  atord  32990  atcvat2  32991  chirred  32997  mdsym  33014  mddmdin0i  33033  cdj1i  33035  fmptcof2  33251  fnpreimac  33264  isoun  33295  fcobijfs  33313  fcobijfs2  33314  lt2addrd  33342  xlt2addrd  33351  xrge0infss  33352  infxrge0glb  33357  xrofsup  33359  fz1nnct  33393  toslublem  33533  tosglblem  33535  ismntd  33545  mgccole1  33551  mgccole2  33552  mgcmnt1  33553  mgcmnt2  33554  dfmgc2lem  33556  dfmgc2  33557  psgnfzto1stlem  33661  fzto1st  33664  psgnfzto1st  33666  trsp2cyc  33684  xrnarchi  33745  archirng  33749  archiexdiv  33751  archiabl  33759  isarchiofld  33760  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnlem4  33806  elrgspn  33807  elrgspnsubrunlem1  33808  elrgspnsubrunlem2  33809  elrgspnsubrun  33810  linds2eq  33936  elrspunidl  33978  elrspunsn  33979  isrprm  34049  evl1deg1  34108  evl1deg2  34109  evl1deg3  34110  0mplrim  34146  selvply1rhmlema  34150  selvply1rhmlemb  34151  selvply1rhmlem1  34152  selvply1rhmlem2  34153  selvply1rhmlem4  34155  selvply1rhm0  34158  extvfvvcl  34167  extvfvcl  34168  mplmulmvr  34171  evlextv  34174  mplvrpmlem  34175  mplvrpmfgalem  34176  mplvrpmga  34177  mplvrpmmhm  34178  mplvrpmrhm  34179  psrmonmul  34182  psrmonprod  34184  esplyfval0  34196  esplylem  34198  esplyfv1  34201  esplyfval3  34204  esplyfvaln  34206  esplyind  34207  ply1degltdimlem  34254  lbsdiflsp0  34258  fedgmullem1  34261  fedgmullem2  34262  fedgmul  34263  fldextrspunlsplem  34305  fldextrspunlsp  34306  smatrcl  34428  smatlem  34429  madjusmdetlem2  34460  madjusmdet  34463  cmpcref  34482  ldlfcntref  34486  dispcmp  34491  zarcmplem  34513  ordtrest2NEWlem  34554  ordtconnlem1  34556  xrge0iifiso  34567  rge0scvg  34581  gsumesum  34691  esumfsup  34702  esumpinfval  34705  esumpcvgval  34710  esumcvg  34718  sigaclcu  34749  sigaclci  34764  unelsiga  34766  unelldsys  34791  sigapildsys  34795  ldgenpisyslem1  34796  fiunelros  34807  measvun  34842  voliune  34862  volfiniune  34863  oms0  34929  omssubaddlem  34931  omssubadd  34932  carsgsigalem  34947  carsgclctunlem2  34951  carsgclctun  34953  pmeasmono  34956  pmeasadd  34957  orvcval2  35091  dstfrvel  35106  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemsv  35142  ballotlemsf1o  35146  breprexp  35262  tgoldbachgt  35292  bnj23  35349  bnj1185  35423  bnj1152  35628  bnj1418  35670  soinfdom  35717  fnrelpredd  35720  weexenwe  35756  kardval2  35821  elkarden  35823  kardeng  35825  kardnnfi  35837  rankkardu  35839  dfdm5  36537  dfrn5  36538  wzel  36586  wsuclem  36587  brpprod  36647  brsset  36651  brbigcup  36660  dffix2  36667  elfuns  36677  brimageg  36689  brdomaing  36697  brrangeg  36698  brimg  36699  brapply  36700  lemsuccf  36703  funpartlem  36706  brrestrict  36713  dfrecs2  36714  dfrdg4  36715  brofs  36770  btwncomim  36778  btwnintr  36784  btwnexch3  36785  btwnexch2  36788  brifs  36808  brcolinear2  36823  colineardim1  36826  brfs  36844  btwnconn1  36866  segcon2  36870  seglerflx  36877  seglemin  36878  btwnsegle  36882  colinbtwnle  36883  broutsideof2  36887  fvray  36906  lineunray  36912  lineelsb2  36913  linerflx1  36914  trer  37104  elicc3  37105  finminlem  37106  nn0prpwlem  37110  nn0prpw  37111  fnessref  37145  refssfne  37146  weiunlem  37251  weiunfrlem  37252  weiunfr  37255  weiunse  37256  unblimceq0lem  37372  unblimceq0  37373  unbdqndv2  37377  knoppndvlem21  37398  taupilemrplb  38242  dfgcd3  38246  icorempo  38275  icoreval  38277  iooelexlt  38286  relowlssretop  38287  domalom  38328  ctbssinf  38330  pibt2  38341  phpreu  38528  fin2solem  38530  fin2so  38531  ltflcei  38532  ptrecube  38539  poimirlem1  38540  poimirlem2  38541  poimirlem5  38544  poimirlem6  38545  poimirlem7  38546  poimirlem9  38548  poimirlem12  38551  poimirlem22  38561  poimirlem23  38562  poimirlem24  38563  poimirlem26  38565  poimirlem27  38566  poimirlem32  38571  heicant  38574  mblfinlem1  38576  mblfinlem2  38577  itg2addnclem  38590  itg2addnclem3  38592  itg2addnc  38593  itg2gt0cn  38594  ibladdnclem  38595  iblmulc2nc  38604  itgabsnc  38608  ftc1anclem5  38616  ftc1anclem7  38618  ftc1anclem8  38619  ftc1anc  38620  indexdom  38669  filbcmb  38675  fdc  38680  prdsbnd  38728  heiborlem3  38748  rrnequiv  38770  rngoueqz  38875  eqbrtr  39171  elrnressn  39213  inxprnres  39231  presucmap  39428  eqvreltr  39624  prtlem10  39923  lsatcveq0  40090  lsatcv1  40106  oposlem  40240  opnlen0  40246  lub0N  40247  glb0N  40251  omllaw  40301  cmtbr4N  40313  cvrval  40327  cvrnbtwn  40329  cvrnbtwn2  40333  cvrnbtwn3  40334  cvrcon3b  40335  cvrnbtwn4  40337  atcvreq0  40372  atnle  40375  atlatmstc  40377  cvlexch1  40386  glbconN  40435  hlsuprexch  40439  exatleN  40462  cvratlem  40479  atcvrj0  40486  atcvrj2b  40490  atlelt  40496  cvrat4  40501  3dim1lem5  40524  3dim2  40526  3dim3  40527  ps-2  40536  llni  40566  llnn0  40574  llnle  40576  lplni  40590  lplni2  40595  lplnle  40598  lplnn0N  40605  llncvrlpln  40616  2llnjN  40625  lvoli  40633  lvoli3  40635  lvoli2  40639  lvoln0N  40649  4at  40671  lplncvrlvol  40674  2lplnj  40678  dalemcea  40718  dalem3  40722  psubspi  40805  linepsubN  40810  elpmap  40816  pmapsub  40826  lnatexN  40837  cdlema1N  40849  cdlemb  40852  elpadd  40857  paddvaln0N  40859  paddasslem5  40882  llnexchb2lem  40926  llnexch2N  40928  islhp  41054  lhpat3  41104  4atexlemex2  41129  4atex  41134  4atex2-0aOLDN  41136  4atex2-0cOLDN  41138  lautle  41142  lautcvr  41150  lauteq  41153  ldilval  41171  ltrnu  41179  trlval2  41221  trlne  41243  cdleme0ex1N  41281  cdleme0nex  41348  cdleme18d  41353  cdlemednuN  41358  cdleme25b  41412  cdleme25cv  41416  cdleme27b  41426  cdleme29b  41433  cdleme31sn  41438  cdleme31fv  41448  cdleme31fv2  41451  cdlemefrs29bpre0  41454  cdlemefr29bpre0N  41464  cdlemefr29clN  41465  cdlemefr32fvaN  41467  cdlemefr32fva1  41468  cdlemefs29pre00N  41470  cdlemefs32sn1aw  41472  cdlemefs29bpre0N  41474  cdlemefs29bpre1N  41475  cdlemefs29cpre1N  41476  cdlemefs29clN  41477  cdlemefs32fvaN  41480  cdlemefs32fva1  41481  cdleme41sn3a  41491  cdleme32fva  41495  cdleme32e  41503  cdleme35f  41512  cdleme40v  41527  cdleme42b  41536  trlord  41627  cdlemg1cex  41646  diaval  42090  diaeldm  42094  diaelrnN  42103  cdlemm10N  42176  dibglbN  42224  dicval  42234  dicfnN  42241  dicvalrelN  42243  dihval  42290  dihlsscpre  42292  dihglblem3N  42353  dihmeetlem2N  42357  djhcvat42  42473  lcmineqlem4  43083  aks4d1p4  43130  aks4d1p5  43131  aks4d1p7  43134  aks4d1p8d2  43136  aks4d1p8  43138  hashnexinjle  43180  sticksstones1  43197  sticksstones2  43198  sticksstones10  43206  sticksstones12a  43208  aks6d1c7lem4  43234  aks6d1c7  43235  grpods  43245  unitscyglem2  43247  unitscyglem3  43248  unitscyglem4  43249  qsalrel  43293  supinf  43294  dvdsexpnn0  43387  redvmptabs  43412  sn-nnne0  43525  sn-sup2  43556  fimgmcyclem  43598  lzenom  43781  fphpdo  43824  irrapxlem4  43832  pellexlem6  43841  infmrgelbi  43885  pellfundre  43888  pellfundlb  43891  monotoddzz  43950  zindbi  43953  jm2.27  44015  rmydioph  44021  rpnnen3lem  44038  aomclem8  44063  hbtlem5  44130  hbt  44132  sdomne0  44414  sdomne0d  44415  ensucne0  44530  sucomisnotcard  44545  en2pr  44548  pr2cv  44549  refimssco  44607  rfovfvfvd  45003  rfovcnvf1od  45004  fsovrfovd  45009  nzss  45301  relprel  45941  permaxinf2lem  46002  wessf1ornlem  46200  axccdom  46235  dmrelrnrel  46239  axccd  46241  rnmptlb  46255  rnmptbdd  46257  rnmptbd2  46261  rnmptbdlem  46267  rnmptbd  46268  dstregt0  46298  suplesup  46351  supxrunb3  46410  supxrleubrnmpt  46416  rexabslelem  46428  rexabsle  46429  suprleubrnmpt  46432  infrnmptle  46433  infxrunb3rnmpt  46438  infxrpnf  46456  supminfxr  46474  infrpgernmpt  46475  xrpnf  46495  limsupre  46651  limsupref  46695  limsupbnd1f  46696  limsuppnfd  46712  climinf2  46717  limsuppnf  46721  climinfmpt  46725  climinf3  46726  limsupmnflem  46730  limsupmnf  46731  limsupre2  46735  limsupmnfuzlem  46736  limsupre2mpt  46740  limsupre3lem  46742  limsupre3  46743  limsupre3mpt  46744  limsupre3uzlem  46745  limsupre3uz  46746  limsupreuz  46747  limsupreuzmpt  46749  liminfval2  46778  liminfreuzlem  46812  liminfreuz  46813  xlimpnfxnegmnf  46824  cnrefiisplem  46839  xlimpnfv  46848  xlimpnf  46852  xlimpnfmpt  46854  dfxlim2  46858  icccncfext  46897  cncficcgt0  46898  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  stoweidlem5  47015  stoweidlem20  47030  stoweidlem26  47036  stoweidlem28  47038  stoweidlem29  47039  stoweidlem34  47044  wallispilem3  47077  stirlinglem13  47096  fourierdlem41  47158  fourierdlem42  47159  fourierdlem51  47167  fourierdlem54  47170  salunicl  47326  saluncl  47327  salexct  47344  salexct2  47349  salexct3  47352  salgencntex  47353  salgensscntex  47354  sge0pnffigt  47406  meadjuni  47467  omeunile  47515  ovnlerp  47572  hoidifhspval  47618  ovolval5lem2  47663  salpreimagelt  47717  pimincfltioo  47728  salpreimagtge  47735  salpreimagtlt  47740  incsmf  47752  issmfgt  47766  smfpreimagt  47772  decsmf  47777  issmfge  47780  smfpimgtxr  47790  smfpreimage  47792  smfinflem  47827  smfinf  47828  finfdm  47856  funressnfv  48113  funressnvmo  48115  funressnmo  48116  dfdfat2  48198  tz6.12-afv  48243  funressndmafv2rn  48293  tz6.12-afv2  48310  dfatcolem  48325  dfatco  48326  zplusmodne  48419  m1modne  48424  minusmod5ne  48425  submodneaddmod  48427  modmknepk  48438  iccpartigtl  48505  iccpartgt  48509  icceuelpartlem  48517  iccpartnel  48520  sprsymrelfolem2  48575  nprmmul2  48610  goldbachthlem2  48631  odz2prm2pw  48648  fmtnoprmfac1  48650  fmtnoprmfac2  48652  fmtnofac2  48654  fmtno4prmfac  48657  fmtno4prm  48660  prmdvdsfmtnof1lem1  48669  31prm  48682  nprmdvdsfacm1  48709  perfectALTVlem2  48820  nnsum3primes4  48886  nnsum3primesprm  48888  nnsum3primesgbe  48890  nnsum3primesle9  48892  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  wtgoldbnnsum4prm  48900  bgoldbnnsum3prm  48902  bgoldbtbndlem4  48906  bgoldbtbnd  48907  tgblthelfgott  48913  tgoldbach  48915  assintop  49306  isassintop  49307  assintopcllaw  49309  ztprmneprm  49459  ply1mulgsumlem1  49498  ply1mulgsumlem2  49499  lco0  49539  lcoel0  49540  lincsumcl  49543  lincscmcl  49544  lcoss  49548  linindslinci  49560  lindslinindsimp1  49569  linds0  49577  el0ldep  49578  lindsrng01  49580  ldepspr  49585  islindeps2  49595  isldepslvec2  49597  zlmodzxzldep  49616  ldepsnlinc  49620  elbigo2r  49665  xpco2  49967  tposres0  49985  lubsscl  50068  glbsscl  50069  lubprlem  50070  ipolub  50096  ipoglb  50099  catprslem  50118  infsubc2  50169  nelsubc3lem  50178  cnelsubclem  50711