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  8250  rntpos  8257  tpostpos  8264  frrlem12  8316  ertr  8734  ecopovsym  8841  ecopovtrn  8842  isfi  9003  en0  9046  en0ALT  9047  en1  9052  endisj  9084  xpcomco  9087  sbth  9117  2pwne  9153  disjenex  9155  ssenen  9171  findcard  9180  findcard2  9181  pssnn  9185  sbthfi  9215  nneneq  9222  php  9223  onomeneq  9230  sdom1  9242  1sdom2dom  9246  isinf  9257  fineqvlem  9258  en1eqsnbi  9268  findcard3  9275  frfi  9277  fiint  9319  mapfienlem1  9398  mapfienlem2  9399  mapfienlem3  9400  mapfien  9401  marypha1lem  9426  supmo  9445  eqsup  9449  supub  9452  suplub  9453  suppr  9465  supisolem  9467  supisoex  9468  infmin  9489  infmo  9490  fiinfg  9494  fiinf2g  9495  infpr  9498  ordtypecbv  9512  ordtypelem3  9515  ordtypelem6  9518  ordtypelem7  9519  ordtypelem9  9521  ordtypelem10  9522  hartogslem1  9537  hartogs  9539  wemaplem1  9541  wemaplem2  9542  wemapso2lem  9547  card2on  9549  card2inf  9550  elharval  9556  brwdom2  9568  wdomtr  9570  cantnfs  9668  cantnfp1lem2  9681  oemapso  9684  cantnflem1  9691  wemapwe  9699  ttrclss  9722  r111  9783  kardexOLD  9959  karden  9960  kardenOLD  9961  setrec2lem1  9975  isnumi  10028  tskwe  10032  cardid2  10035  cardonle  10039  cardne  10047  iscard2  10058  infxpenlem  10093  fodomfi2  10140  wdomfil  10141  wdomnumr  10144  alephsuc2  10160  infenaleph  10171  iunfictbso  10194  infpss  10295  cff1  10337  cfslb2n  10347  sornom  10356  fin4i  10377  isfin6  10379  isfin7  10380  isfin1-3  10465  fin1a2lem9  10487  fin1a2lem11  10489  hsmexlem4  10508  axcc2lem  10515  axcc4dom  10520  domtriomlem  10521  numthcor  10573  zorn2lem2  10576  zorn2lem3  10577  zorn2lem7  10581  zorn2g  10582  axdclem  10598  axdc  10600  brdom7disj  10611  brdom6disj  10612  uniimadom  10629  ondomon  10648  alephval2  10658  alephreg  10668  pwcfsdom  10669  elgch  10708  gchi  10710  fpwwe2lem11  10727  fpwwe2lem12  10728  winainflem  10779  winalim2  10782  tsken  10840  0tsk  10841  inar1  10861  tskord  10866  tskuni  10869  grudomon  10903  pinq  11013  nqereu  11015  enqeq  11020  ltbtwnnq  11064  ltrnq  11065  prcdnq  11079  prnmax  11081  genpnmax  11093  nqpr  11100  1idpr  11115  reclem2pr  11134  reclem3pr  11135  reclem4pr  11136  recexpr  11137  supexpr  11140  ltsosr  11180  1ne0sr  11182  ltasr  11186  supsrlem  11197  axpre-lttri  11251  axpre-lttrn  11252  axpre-ltadd  11253  axpre-sup  11255  lelttr  11401  dedekind  11474  dedekindle  11475  ltordlem  11842  lt0ne0d  11882  fimaxre3  12264  fiminre2  12266  lbreu  12268  lble  12270  sup2  12274  infm3  12277  suprleub  12284  supaddc  12285  supadd  12286  supmul1  12287  supmullem1  12288  supmul  12290  nnne0  12373  nnsub  12383  nominpos  12584  nnunb  12603  arch  12604  nn0sub  12657  nn0n0n1ge2b  12676  nn0lt10b  12762  zextle  12773  peano5uzti  12790  fzind  12798  btwnz  12803  uzval  12968  uzwo  13039  nnwof  13042  ublbneg  13061  lbzbi  13064  zsupss  13065  uzsupss  13068  uzwo3  13071  zmax  13073  rebtwnz  13075  rpnnen1lem3  13108  xrltnsym  13267  xrlttri  13269  xrlttr  13270  xrlelttr  13286  nltpnft  13295  xrmaxlt  13312  xrmaxle  13314  qbtwnre  13330  qbtwnxr  13331  xltnegi  13347  xnn0lenn0nn0  13376  xsubge0  13392  xlesubadd  13394  xmullem2  13396  xlemul1a  13419  xrinfmexpnf  13437  xrsupsslem  13438  xrinfmsslem  13439  xrub  13443  supxrunb1  13450  supxrunb2  13451  reltre  13472  rpltrp  13473  reltxrnmnf  13474  ixxval  13485  elixx1  13486  elioo2  13518  iccid  13522  icc0  13525  fzval  13642  elfz1  13645  elfznelfzo  13909  elfznelfzob  13910  flval  13935  fllelt  13938  flflp1  13948  flval2  13955  flval3  13956  flbi  13957  dfceil2  13980  ceilval2  13981  fleqceilz  13995  modid2  14039  addmodlteq  14090  fsequb2  14120  ssnn0fi  14129  seqf1olem2  14186  sqlecan  14354  faclbnd4lem1  14438  hashsnle1  14563  pr2pwpr  14625  hash3tpde  14639  rtrclreclem3  15214  relexpindlem  15217  sgnval  15242  sgnmulsgn  15263  01sqrexlem6  15415  01sqrex  15417  abslt  15483  absle  15484  rexanre  15515  rexico  15522  limsupgle  15645  limsupgre  15649  limsupbnd2  15651  rlim2lt  15665  rlim3  15666  ello12r  15685  ello1d  15691  elo12r  15696  rlimconst  15712  climshft  15744  rlimcn3  15758  o1rlimmul  15787  lo1le  15820  climsup  15838  caucvgrlem  15841  isumless  16015  divrcnv  16022  cvgrat  16053  rpnnen2lem10  16392  ruclem1  16400  ruclem2  16401  ruclem11  16409  ruclem12  16410  sqrt2irr  16418  absdvdsb  16445  dvdsle  16481  dvdsabseq  16484  dvdsdivcl  16487  dvdsext  16492  divalglem8  16571  divalglem9  16572  divalglem10  16573  divalgmod  16577  ndvdssub  16580  sadcaddlem  16628  gcdcllem1  16670  gcdcllem2  16671  gcdcllem3  16672  dfgcd2  16720  gcdzeq  16726  dvdssq  16743  nn0seqcvgd  16746  algcvgblem  16753  lcmval  16768  lcmdvds  16784  lcmgcdeq  16788  lcmfpr  16803  lcmf  16809  lcmftp  16812  lcmfunsnlem1  16813  lcmfunsnlem2lem1  16814  lcmfunsnlem2lem2  16815  lcmfdvdsb  16819  coprmgcdb  16825  coprmdvds1  16828  1nprm  16855  1idssfct  16856  isprm2lem  16857  isprm2  16858  dvdsprime  16863  nprm  16864  3prm  16870  dvdsprm  16880  exprmfct  16881  isprm5  16884  maxprmfct  16886  coprm  16888  prmdvdsncoprmbd  16904  ncoprmlnprm  16905  eulerthlem2  16960  phisum  16969  odzval  16970  pythagtriplem4  16998  pc2dvds  17058  pcprmpw2  17061  pcprmpw  17062  dvdsprmpweqle  17065  oddprmdvds  17082  prmpwdvds  17083  pockthg  17085  unbenlem  17087  prmreclem4  17098  prmreclem5  17099  prmreclem6  17100  1arith  17106  vdwlem6  17165  vdwlem11  17170  vdwlem13  17172  ramtlecl  17179  ramub  17192  rami  17194  ramubcl  17197  0ram  17199  ram0  17201  prmdvdsprmop  17222  prmolefac  17225  prmodvdslcmf  17226  prmgaplem2  17229  prmgaplcmlem1  17230  prmgaplcmlem2  17231  prmgaplem3  17232  prmgaplem4  17233  prmgaplem5  17234  prmgaplem6  17235  prmgapprmolem  17240  prmlem0  17284  prmlem1a  17285  imasaddfnlem  17701  imasvscafn  17710  imasleval  17714  prslem  18472  drsdir  18477  drsdirfi  18480  isdrs2  18481  posi  18492  posasymb  18494  pospropd  18500  pltval3  18512  plelttr  18517  pospo  18518  lubprop  18531  luble  18532  lublecllem  18533  glbprop  18544  joinval2lem  18553  joinlem  18556  meetlem  18570  meetle  18573  poslubmo  18584  posglbmo  18585  poslubd  18586  tleile  18594  latnlej  18631  isglbd  18684  lubub  18686  lubun  18690  clatleglb  18693  tsrlin  18760  letsr  18768  dirge  18778  pmtrval  19666  pmtrrn  19672  pmtrfrn  19673  pmtrrn2  19675  pmtrsn  19734  mndodcongi  19758  odeq  19765  odmulgeq  19772  gexnnod  19803  sylow1lem1  19813  pgpssslw  19829  sylow2a  19834  efgredeu  19967  efgred2  19968  gexex  20068  frgpnabllem2  20089  cyggenod  20099  dprdval  20220  dprdw  20227  dprdwd  20228  ablfacrplem  20282  ablfac1c  20288  ablfac1eu  20290  ablfaclem3  20304  omndadd  20343  abvtrivd  21090  zringlpir  21774  prmirredlem  21779  znleval  21861  frlmelbas  22063  ellspd  22109  islindf4  22145  psrbagconcl  22236  psrbagleadd1  22237  gsumbagdiaglem  22240  rhmpsrlem2  22250  psrlidm  22270  psrridm  22271  psrass1  22272  psrcom  22276  mplelbas  22299  mplmonmul  22346  ltbwe  22354  mhpmulcl  22471  psdmul  22488  coe1fsupp  22533  coe1ae0  22535  coe1mul2  22589  coe1tmmul  22597  pmatcoe1fsupp  23020  chfacffsupp  23175  chfacfscmulfsupp  23178  chfacfscmulgsum  23179  chfacfpmmulfsupp  23182  chfacfpmmulgsum  23183  ordtbas2  23510  ordtopn2  23514  ordtrest2lem  23522  pnfnei  23539  ordtt1  23698  ordthauslem  23702  2ndci  23767  2ndcsb  23768  2ndcredom  23769  2ndc1stc  23770  1stcrest  23772  2ndcctbss  23775  2ndcdisj  23776  2ndcsep  23779  lly1stc  23816  tx1stc  23970  ordthmeolem  24121  ufildom1  24246  xmetrtri2  24676  prdsxmetlem  24688  ssblex  24748  prdsbl  24811  comet  24833  stdbdxmet  24835  stdbdmopn  24838  met1stc  24841  dscmet  24892  metdstri  25172  metdscn  25177  xrhmeo  25268  bndth  25280  evth  25281  lebnumlem3  25285  pcovalg  25334  pco1  25337  pcocn  25339  pcopt  25344  pcopt2  25345  pcoass  25346  nmoleub3  25441  bcthlem5  25650  rrxfsupp  25724  minveclem4c  25747  minveclem2  25748  minveclem3b  25750  minveclem4  25754  minveclem6  25756  pmltpclem1  25770  pmltpc  25772  ovollb2lem  25810  ovolctb  25812  ovolunlem1  25819  ovoliunlem1  25824  ovoliunlem2  25825  ovoliun2  25828  ovolshftlem1  25831  ovolscalem1  25835  ovolicc1  25838  ovolicc2lem3  25841  voliunlem2  25873  voliunlem3  25874  ioombl1lem4  25883  uniioovol  25901  uniioombllem2  25905  uniioombllem3  25907  uniioombllem6  25910  volsup2  25927  ismbfd  25961  mbfsup  25986  mbflimsup  25988  itg1climres  26036  mbfi1fseqlem4  26040  itg2lr  26052  itg2leub  26056  itg2seq  26064  itg2monolem1  26072  itg2monolem3  26074  itg2mono  26075  itg2i1fseq2  26078  itg2gt0  26082  itg2cnlem1  26083  itg2cnlem2  26084  itg2cn  26085  iblss  26126  itgless  26138  ibladdlem  26141  iblabsr  26151  iblmulc2  26152  itgabs  26156  bddiblnc  26163  ditgeq1  26169  dvferm2lem  26307  rolle  26311  dvlip2  26316  c1liplem1  26317  c1lip1  26318  dvfsumlem2  26348  dvfsumlem4  26350  mdegleb  26383  degltlem1  26391  plyco0  26511  plyeq0lem  26530  coeeq2  26562  dgrle  26563  dgradd2  26588  plydiveu  26620  aareccl  26654  aalioulem2  26661  aaliou3lem7  26677  psercnlem1  26753  pilem2  26780  pilem3  26781  logltb  26929  divlogrlim  26964  logcnlem3  26973  cxpaddlelem  27080  rlimcnp  27294  cxplim  27300  cxploglim  27306  scvxcvx  27314  ftalem1  27401  ftalem2  27402  isppw2  27443  vmappw  27444  sgmnncl  27475  sqff1o  27510  fsumdvdsdiaglem  27511  dvdsppwf1o  27514  dvdsflsumcom  27516  musum  27519  muinv  27521  mpodvdsmulf1o  27522  dvdsmulf1o  27524  vmalelog  27533  vmasum  27544  logfac2  27545  perfectlem2  27558  bcmono  27605  bpos1lem  27610  bposlem9  27620  lgsmod  27651  lgsne0  27663  gausslemma2dlem4  27697  2sqlem6  27751  2sqlem8  27754  2sqlem10  27756  2sqreulem1  27774  2sqreunnlem1  27777  chtppilim  27803  rpvmasumlem  27815  dchrisumlema  27816  dchrisumlem2  27818  dchrvmasumlem1  27823  dchrvmasumiflem1  27829  dchrisum0flblem1  27836  dchrisum0flblem2  27837  dchrisum0  27848  rplogsum  27855  logsqvma  27870  pntpbnd1  27914  pntpbnd2  27915  pntibndlem3  27920  pntlemj  27931  pntlemi  27932  pntlem3  27937  pnt3  27940  ostth3  27966  flt4lem2  27978  flt4lem7  27990  nodense  28050  noresle  28055  nosupprefixmo  28058  noinfprefixmo  28059  nosupcbv  28060  nosupdm  28062  nosupbnd1lem1  28066  nosupbnd1lem4  28069  nosupbnd1  28072  nosupbnd2lem1  28073  nosupbnd2  28074  noinfcbv  28075  noinfdm  28077  noinffv  28079  noinfres  28080  noinfbnd1lem3  28083  noinfbnd1lem4  28084  noinfbnd1lem5  28085  noinfbnd1  28087  noetalem2  28100  nocvxminlem  28141  sltssnb  28156  sltssepc  28158  conway  28166  cutsval  28167  etaslts  28180  lesrec  28186  eqcuts3  28191  bday1  28201  cuteq1  28204  madeval2  28220  rightval  28237  elleft  28238  sltsright  28248  made0  28250  madecut  28270  left1s  28282  madebdaylemlrcut  28286  ltslpss  28295  cofslts  28305  coinitslts  28306  cofcutr  28311  cofcutrtime  28314  cofss  28317  coiniss  28318  cutmax  28321  cutmin  28322  cutminmax  28323  addsproplem1  28356  addsprop  28363  leadds1  28376  addsuniflem  28388  negsproplem1  28415  negsprop  28422  negsid  28428  negsunif  28442  mulsproplemcbv  28502  mulsproplem1  28503  mulsproplem9  28511  mulsprop  28517  sltmuls1  28534  sltmuls2  28535  mulsuniflem  28536  precsexlem11  28604  abslts  28636  oncutlt  28651  oniso  28658  bdayons  28663  addonbday  28666  n0fincut  28742  onsfi  28743  n0subs  28750  bdayn0p1  28756  eucliddivs  28763  zcuts  28794  twocut  28810  halfcut  28845  addhalfcut  28846  bdaypw2n0bndlem  28850  bdayfinbndcbv  28853  bdayfinbndlem1  28854  bdayfinbndlem2  28855  z12bdaylem1  28857  elreno  28878  elreno2  28882  tgjustc1  28938  tgjustc2  28939  iscgrglt  28978  tgcgr4  28995  hlcgreu  29085  elplng  29259  plngcplem  29264  lmif  29291  islmib  29293  trgcopyeu  29314  iscgrad  29319  inaghl  29365  axlowdim2  29539  axlowdim  29540  axcontlem2  29544  axcontlem3  29545  axcontlem4  29546  axcontlem7  29549  axcontlem9  29551  axcontlem10  29552  axcontlem11  29553  axcontlem12  29554  ebtwntg  29561  umgrupgr  29682  nbusgrvtxm1  29961  crctcshwlkn0lem2  30401  crctcshwlkn0lem3  30402  crctcsh  30414  wlkswwlksf1o  30469  clwlkclwwlklem2fv1  30587  clwlkclwwlkf  30600  0clwlkv  30723  loop1cycl  30745  umgr2cycl  30748  acycgrcycl  30754  eupth2  30841  numclwwlk5  30990  nmoubi  31375  minvecolem2  31478  minvecolem3  31479  minvecolem4c  31482  minvecolem4  31483  minvecolem5  31484  minvecolem6  31485  htthlem  31520  chlimi  31837  chcompl  31845  hsn0elch  31851  cmbr3  32211  cmcm  32217  cmcm3  32218  lecm  32220  nmopub  32511  nmfnleub  32528  nmopun  32617  nmcexi  32629  cnlnadjlem7  32676  pjnmopi  32751  stle0i  32842  stlesi  32844  stm1i  32846  csmdsymi  32937  cvmd  32939  atcveq0  32951  atcv1  32983  atord  32991  atcvat2  32992  chirred  32998  mdsym  33015  mddmdin0i  33034  cdj1i  33036  fmptcof2  33294  fnpreimac  33307  isoun  33338  fcobijfs  33356  fcobijfs2  33357  lt2addrd  33385  xlt2addrd  33394  xrge0infss  33395  infxrge0glb  33400  xrofsup  33402  fz1nnct  33436  toslublem  33576  tosglblem  33578  ismntd  33588  mgccole1  33594  mgccole2  33595  mgcmnt1  33596  mgcmnt2  33597  dfmgc2lem  33599  dfmgc2  33600  psgnfzto1stlem  33704  fzto1st  33707  psgnfzto1st  33709  trsp2cyc  33727  xrnarchi  33788  archirng  33792  archiexdiv  33794  archiabl  33802  isarchiofld  33803  elrgspnlem1  33846  elrgspnlem2  33847  elrgspnlem3  33848  elrgspnlem4  33849  elrgspn  33850  elrgspnsubrunlem1  33851  elrgspnsubrunlem2  33852  elrgspnsubrun  33853  linds2eq  33979  elrspunidl  34021  elrspunsn  34022  isrprm  34092  evl1deg1  34151  evl1deg2  34152  evl1deg3  34153  0mplrim  34189  selvply1rhmlema  34193  selvply1rhmlemb  34194  selvply1rhmlem1  34195  selvply1rhmlem2  34196  selvply1rhmlem4  34198  selvply1rhm0  34201  extvfvvcl  34210  extvfvcl  34211  mplmulmvr  34214  evlextv  34217  mplvrpmlem  34218  mplvrpmfgalem  34219  mplvrpmga  34220  mplvrpmmhm  34221  mplvrpmrhm  34222  psrmonmul  34225  psrmonprod  34227  esplyfval0  34239  esplylem  34241  esplyfv1  34244  esplyfval3  34247  esplyfvaln  34249  esplyind  34250  ply1degltdimlem  34297  lbsdiflsp0  34301  fedgmullem1  34304  fedgmullem2  34305  fedgmul  34306  fldextrspunlsplem  34348  fldextrspunlsp  34349  smatrcl  34471  smatlem  34472  madjusmdetlem2  34503  madjusmdet  34506  cmpcref  34525  ldlfcntref  34529  dispcmp  34534  zarcmplem  34556  ordtrest2NEWlem  34597  ordtconnlem1  34599  xrge0iifiso  34610  rge0scvg  34624  gsumesum  34734  esumfsup  34745  esumpinfval  34748  esumpcvgval  34753  esumcvg  34761  sigaclcu  34792  sigaclci  34807  unelsiga  34809  unelldsys  34834  sigapildsys  34838  ldgenpisyslem1  34839  fiunelros  34850  measvun  34885  voliune  34905  volfiniune  34906  oms0  34972  omssubaddlem  34974  omssubadd  34975  carsgsigalem  34990  carsgclctunlem2  34994  carsgclctun  34996  pmeasmono  34999  pmeasadd  35000  orvcval2  35134  dstfrvel  35149  ballotlemfc0  35168  ballotlemfcc  35169  ballotlemsv  35185  ballotlemsf1o  35189  breprexp  35305  tgoldbachgt  35335  bnj23  35392  bnj1185  35466  bnj1152  35671  bnj1418  35713  soinfdom  35760  fnrelpredd  35763  weexenwe  35799  kardval2  35864  elkarden  35866  kardeng  35868  kardnnfi  35880  rankkardu  35882  dfdm5  36580  dfrn5  36581  wzel  36629  wsuclem  36630  brpprod  36690  brsset  36694  brbigcup  36703  dffix2  36710  elfuns  36720  brimageg  36732  brdomaing  36740  brrangeg  36741  brimg  36742  brapply  36743  lemsuccf  36746  funpartlem  36749  brrestrict  36756  dfrecs2  36757  dfrdg4  36758  brofs  36813  btwncomim  36821  btwnintr  36827  btwnexch3  36828  btwnexch2  36831  brifs  36851  brcolinear2  36866  colineardim1  36869  brfs  36887  btwnconn1  36909  segcon2  36913  seglerflx  36920  seglemin  36921  btwnsegle  36925  colinbtwnle  36926  broutsideof2  36930  fvray  36949  lineunray  36955  lineelsb2  36956  linerflx1  36957  trer  37147  elicc3  37148  finminlem  37149  nn0prpwlem  37153  nn0prpw  37154  fnessref  37188  refssfne  37189  weiunlem  37294  weiunfrlem  37295  weiunfr  37298  weiunse  37299  unblimceq0lem  37415  unblimceq0  37416  unbdqndv2  37420  knoppndvlem21  37441  taupilemrplb  38285  dfgcd3  38289  icorempo  38318  icoreval  38320  iooelexlt  38329  relowlssretop  38330  domalom  38371  ctbssinf  38373  pibt2  38384  phpreu  38571  fin2solem  38573  fin2so  38574  ltflcei  38575  ptrecube  38582  poimirlem1  38583  poimirlem2  38584  poimirlem5  38587  poimirlem6  38588  poimirlem7  38589  poimirlem9  38591  poimirlem12  38594  poimirlem22  38604  poimirlem23  38605  poimirlem24  38606  poimirlem26  38608  poimirlem27  38609  poimirlem32  38614  heicant  38617  mblfinlem1  38619  mblfinlem2  38620  itg2addnclem  38633  itg2addnclem3  38635  itg2addnc  38636  itg2gt0cn  38637  ibladdnclem  38638  iblmulc2nc  38647  itgabsnc  38651  ftc1anclem5  38659  ftc1anclem7  38661  ftc1anclem8  38662  ftc1anc  38663  indexdom  38712  filbcmb  38718  fdc  38723  prdsbnd  38771  heiborlem3  38791  rrnequiv  38813  rngoueqz  38918  eqbrtr  39214  elrnressn  39256  inxprnres  39274  presucmap  39471  eqvreltr  39667  prtlem10  39966  lsatcveq0  40133  lsatcv1  40149  oposlem  40283  opnlen0  40289  lub0N  40290  glb0N  40294  omllaw  40344  cmtbr4N  40356  cvrval  40370  cvrnbtwn  40372  cvrnbtwn2  40376  cvrnbtwn3  40377  cvrcon3b  40378  cvrnbtwn4  40380  atcvreq0  40415  atnle  40418  atlatmstc  40420  cvlexch1  40429  glbconN  40478  hlsuprexch  40482  exatleN  40505  cvratlem  40522  atcvrj0  40529  atcvrj2b  40533  atlelt  40539  cvrat4  40544  3dim1lem5  40567  3dim2  40569  3dim3  40570  ps-2  40579  llni  40609  llnn0  40617  llnle  40619  lplni  40633  lplni2  40638  lplnle  40641  lplnn0N  40648  llncvrlpln  40659  2llnjN  40668  lvoli  40676  lvoli3  40678  lvoli2  40682  lvoln0N  40692  4at  40714  lplncvrlvol  40717  2lplnj  40721  dalemcea  40761  dalem3  40765  psubspi  40848  linepsubN  40853  elpmap  40859  pmapsub  40869  lnatexN  40880  cdlema1N  40892  cdlemb  40895  elpadd  40900  paddvaln0N  40902  paddasslem5  40925  llnexchb2lem  40969  llnexch2N  40971  islhp  41097  lhpat3  41147  4atexlemex2  41172  4atex  41177  4atex2-0aOLDN  41179  4atex2-0cOLDN  41181  lautle  41185  lautcvr  41193  lauteq  41196  ldilval  41214  ltrnu  41222  trlval2  41264  trlne  41286  cdleme0ex1N  41324  cdleme0nex  41391  cdleme18d  41396  cdlemednuN  41401  cdleme25b  41455  cdleme25cv  41459  cdleme27b  41469  cdleme29b  41476  cdleme31sn  41481  cdleme31fv  41491  cdleme31fv2  41494  cdlemefrs29bpre0  41497  cdlemefr29bpre0N  41507  cdlemefr29clN  41508  cdlemefr32fvaN  41510  cdlemefr32fva1  41511  cdlemefs29pre00N  41513  cdlemefs32sn1aw  41515  cdlemefs29bpre0N  41517  cdlemefs29bpre1N  41518  cdlemefs29cpre1N  41519  cdlemefs29clN  41520  cdlemefs32fvaN  41523  cdlemefs32fva1  41524  cdleme41sn3a  41534  cdleme32fva  41538  cdleme32e  41546  cdleme35f  41555  cdleme40v  41570  cdleme42b  41579  trlord  41670  cdlemg1cex  41689  diaval  42133  diaeldm  42137  diaelrnN  42146  cdlemm10N  42219  dibglbN  42267  dicval  42277  dicfnN  42284  dicvalrelN  42286  dihval  42333  dihlsscpre  42335  dihglblem3N  42396  dihmeetlem2N  42400  djhcvat42  42516  lcmineqlem4  43126  aks4d1p4  43173  aks4d1p5  43174  aks4d1p7  43177  aks4d1p8d2  43179  aks4d1p8  43181  hashnexinjle  43223  sticksstones1  43240  sticksstones2  43241  sticksstones10  43249  sticksstones12a  43251  aks6d1c7lem4  43277  aks6d1c7  43278  grpods  43288  unitscyglem2  43290  unitscyglem3  43291  unitscyglem4  43292  qsalrel  43336  supinf  43337  dvdsexpnn0  43430  redvmptabs  43455  sn-nnne0  43568  sn-sup2  43599  fimgmcyclem  43641  lzenom  43825  fphpdo  43868  irrapxlem4  43876  pellexlem6  43885  infmrgelbi  43929  pellfundre  43932  pellfundlb  43935  monotoddzz  43994  zindbi  43997  jm2.27  44059  rmydioph  44065  rpnnen3lem  44082  aomclem8  44107  hbtlem5  44174  hbt  44176  sdomne0  44458  sdomne0d  44459  ensucne0  44574  sucomisnotcard  44589  en2pr  44592  pr2cv  44593  refimssco  44651  rfovfvfvd  45047  rfovcnvf1od  45048  fsovrfovd  45053  nzss  45345  relprel  45985  permaxinf2lem  46046  wessf1ornlem  46244  axccdom  46279  dmrelrnrel  46283  axccd  46285  rnmptlb  46299  rnmptbdd  46301  rnmptbd2  46305  rnmptbdlem  46311  rnmptbd  46312  dstregt0  46342  suplesup  46395  supxrunb3  46454  supxrleubrnmpt  46460  rexabslelem  46472  rexabsle  46473  suprleubrnmpt  46476  infrnmptle  46477  infxrunb3rnmpt  46482  infxrpnf  46500  supminfxr  46518  infrpgernmpt  46519  xrpnf  46539  limsupre  46695  limsupref  46739  limsupbnd1f  46740  limsuppnfd  46756  climinf2  46761  limsuppnf  46765  climinfmpt  46769  climinf3  46770  limsupmnflem  46774  limsupmnf  46775  limsupre2  46779  limsupmnfuzlem  46780  limsupre2mpt  46784  limsupre3lem  46786  limsupre3  46787  limsupre3mpt  46788  limsupre3uzlem  46789  limsupre3uz  46790  limsupreuz  46791  limsupreuzmpt  46793  liminfval2  46822  liminfreuzlem  46856  liminfreuz  46857  xlimpnfxnegmnf  46868  cnrefiisplem  46883  xlimpnfv  46892  xlimpnf  46896  xlimpnfmpt  46898  dfxlim2  46902  icccncfext  46941  cncficcgt0  46942  ioodvbdlimc1lem2  46986  ioodvbdlimc2lem  46988  stoweidlem5  47059  stoweidlem20  47074  stoweidlem26  47080  stoweidlem28  47082  stoweidlem29  47083  stoweidlem34  47088  wallispilem3  47121  stirlinglem13  47140  fourierdlem41  47202  fourierdlem42  47203  fourierdlem51  47211  fourierdlem54  47214  salunicl  47370  saluncl  47371  salexct  47388  salexct2  47393  salexct3  47396  salgencntex  47397  salgensscntex  47398  sge0pnffigt  47450  meadjuni  47511  omeunile  47559  ovnlerp  47616  hoidifhspval  47662  ovolval5lem2  47707  salpreimagelt  47761  pimincfltioo  47772  salpreimagtge  47779  salpreimagtlt  47784  incsmf  47796  issmfgt  47810  smfpreimagt  47816  decsmf  47821  issmfge  47824  smfpimgtxr  47834  smfpreimage  47836  smfinflem  47871  smfinf  47872  finfdm  47900  funressnfv  48157  funressnvmo  48159  funressnmo  48160  dfdfat2  48242  tz6.12-afv  48287  funressndmafv2rn  48337  tz6.12-afv2  48354  dfatcolem  48369  dfatco  48370  zplusmodne  48463  m1modne  48468  minusmod5ne  48469  submodneaddmod  48471  modmknepk  48482  iccpartigtl  48549  iccpartgt  48553  icceuelpartlem  48561  iccpartnel  48564  sprsymrelfolem2  48619  nprmmul2  48654  goldbachthlem2  48675  odz2prm2pw  48692  fmtnoprmfac1  48694  fmtnoprmfac2  48696  fmtnofac2  48698  fmtno4prmfac  48701  fmtno4prm  48704  prmdvdsfmtnof1lem1  48713  31prm  48726  nprmdvdsfacm1  48753  perfectALTVlem2  48864  nnsum3primes4  48930  nnsum3primesprm  48932  nnsum3primesgbe  48934  nnsum3primesle9  48936  nnsum4primeseven  48942  nnsum4primesevenALTV  48943  wtgoldbnnsum4prm  48944  bgoldbnnsum3prm  48946  bgoldbtbndlem4  48950  bgoldbtbnd  48951  tgblthelfgott  48957  tgoldbach  48959  assintop  49350  isassintop  49351  assintopcllaw  49353  ztprmneprm  49503  ply1mulgsumlem1  49542  ply1mulgsumlem2  49543  lco0  49583  lcoel0  49584  lincsumcl  49587  lincscmcl  49588  lcoss  49592  linindslinci  49604  lindslinindsimp1  49613  linds0  49621  el0ldep  49622  lindsrng01  49624  ldepspr  49629  islindeps2  49639  isldepslvec2  49641  zlmodzxzldep  49660  ldepsnlinc  49664  elbigo2r  49709  xpco2  50011  tposres0  50029  lubsscl  50112  glbsscl  50113  lubprlem  50114  ipolub  50140  ipoglb  50143  catprslem  50162  infsubc2  50213  nelsubc3lem  50222  cnelsubclem  50755