Theorem breq1 5109

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ⟨cop 4838   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  breq12  5111  breq1i  5113  breq1d  5116  nbrne2  5128  brab1  5156  pocl  5571  swopolem  5573  swopo  5574  po2ne  5579  solin  5590  sotrieq  5594  sotr2  5597  isso2i  5600  somo  5602  dffr2  5616  frc  5618  frirr  5631  fr2nr  5632  wereu2  5652  vtoclr  5718  frsn  5744  brcog  5849  brcogw  5851  brcnvg  5863  dfdmf  5884  eldmg  5886  dmun  5898  dm0rn0  5912  dfrnf  5938  dmcosseq  5966  dmcosseqOLD  5967  dfres2  6044  imasng  6093  cotrg  6116  cnvsym  6119  asymref2  6122  sotri2  6134  somin1  6138  rnco  6265  coi1  6278  predtrss  6340  frpomin  6358  dffun2  6565  dffun6f  6570  funmo  6571  fun11  6633  fveq2  6905  eliman0  6942  nfunsn  6944  dffv2  7000  fvopab5  7047  dff3  7121  f1ompt  7132  fmptco  7151  dff13  7278  foeqcnvco  7328  isorel  7354  soisores  7355  soisoi  7356  isocnv  7358  isotr  7364  isomin  7365  isoini  7366  isopolem  7373  isosolem  7375  f1oiso  7379  f1oiso2  7380  weniso  7384  eqfunresadj  7390  caovordig  7647  caovordg  7649  caovord3d  7652  caovord  7653  caovord3  7655  caofrss  7753  caoftrn  7755  fr3nr  7807  dfwe2  7809  f1oweALT  8005  frxp  8162  poxp  8164  fnwe2lem3  8171  fnse  8174  poxp2  8184  frxp2  8185  poxp3  8191  frxp3  8192  xpord3pred  8193  poseq  8199  brtpos2  8274  rntpos  8281  tpostpos  8288  frrlem12  8340  ertr  8758  ecopovsym  8865  ecopovtrn  8866  isfi  9027  en0  9070  en0ALT  9071  en1  9076  endisj  9108  xpcomco  9111  sbth  9141  2pwne  9177  disjenex  9179  ssenen  9195  findcard  9204  findcard2  9205  pssnn  9209  sbthfi  9239  nneneq  9246  php  9247  onomeneq  9254  sdom1  9266  1sdom2dom  9270  isinf  9281  fineqvlem  9282  en1eqsnbi  9292  findcard3  9299  frfi  9301  fiint  9343  mapfienlem1  9421  mapfienlem2  9422  mapfienlem3  9423  mapfien  9424  marypha1lem  9449  supmo  9468  eqsup  9472  supub  9475  suplub  9476  suppr  9488  supisolem  9490  supisoex  9491  infmin  9512  infmo  9513  fiinfg  9517  fiinf2g  9518  infpr  9521  ordtypecbv  9535  ordtypelem3  9538  ordtypelem6  9541  ordtypelem7  9542  ordtypelem9  9544  ordtypelem10  9545  hartogslem1  9560  hartogs  9562  wemaplem1  9564  wemaplem2  9565  wemapso2lem  9570  card2on  9572  card2inf  9573  elharval  9579  brwdom2  9591  wdomtr  9593  cantnfs  9691  cantnfp1lem2  9704  oemapso  9707  cantnflem1  9714  wemapwe  9722  r111  9806  kardexOLD  9982  karden  9983  kardenOLD  9984  setrec2lem1  9998  isnumi  10051  tskwe  10055  cardid2  10058  cardonle  10062  cardne  10070  iscard2  10081  infxpenlem  10116  fodomfi2  10163  wdomfil  10164  wdomnumr  10167  alephsuc2  10183  infenaleph  10194  iunfictbso  10217  infpss  10318  cff1  10360  cfslb2n  10370  sornom  10379  fin4i  10400  isfin6  10402  isfin7  10403  isfin1-3  10488  fin1a2lem9  10510  fin1a2lem11  10512  hsmexlem4  10531  axcc2lem  10538  axcc4dom  10543  domtriomlem  10544  numthcor  10596  zorn2lem2  10599  zorn2lem3  10600  zorn2lem7  10604  zorn2g  10605  axdclem  10621  axdc  10623  brdom7disj  10634  brdom6disj  10635  uniimadom  10652  ondomon  10671  alephval2  10681  alephreg  10691  pwcfsdom  10692  elgch  10731  gchi  10733  fpwwe2lem11  10750  fpwwe2lem12  10751  winainflem  10802  winalim2  10805  tsken  10863  0tsk  10864  inar1  10884  tskord  10889  tskuni  10892  grudomon  10926  pinq  11036  nqereu  11038  enqeq  11043  ltbtwnnq  11087  ltrnq  11088  prcdnq  11102  prnmax  11104  genpnmax  11116  nqpr  11123  1idpr  11138  reclem2pr  11157  reclem3pr  11158  reclem4pr  11159  recexpr  11160  supexpr  11163  ltsosr  11203  1ne0sr  11205  ltasr  11209  supsrlem  11220  axpre-lttri  11274  axpre-lttrn  11275  axpre-ltadd  11276  axpre-sup  11278  lelttr  11424  dedekind  11497  dedekindle  11498  ltordlem  11865  lt0ne0d  11905  fimaxre3  12287  fiminre2  12289  lbreu  12291  lble  12293  sup2  12297  infm3  12300  suprleub  12307  supaddc  12308  supadd  12309  supmul1  12310  supmullem1  12311  supmul  12313  nnne0  12396  nnsub  12406  nominpos  12607  nnunb  12626  arch  12627  nn0sub  12680  nn0n0n1ge2b  12699  nn0lt10b  12785  zextle  12796  peano5uzti  12813  fzind  12821  btwnz  12826  uzval  12991  uzwo  13062  nnwof  13065  ublbneg  13084  lbzbi  13087  zsupss  13088  uzsupss  13091  uzwo3  13094  zmax  13096  rebtwnz  13098  rpnnen1lem3  13131  xrltnsym  13290  xrlttri  13292  xrlttr  13293  xrlelttr  13309  nltpnft  13318  xrmaxlt  13335  xrmaxle  13337  qbtwnre  13353  qbtwnxr  13354  xltnegi  13370  xnn0lenn0nn0  13399  xsubge0  13415  xlesubadd  13417  xmullem2  13419  xlemul1a  13442  xrinfmexpnf  13460  xrsupsslem  13461  xrinfmsslem  13462  xrub  13466  supxrunb1  13473  supxrunb2  13474  reltre  13495  rpltrp  13496  reltxrnmnf  13497  ixxval  13508  elixx1  13509  elioo2  13541  iccid  13545  icc0  13548  fzval  13665  elfz1  13668  elfznelfzo  13932  elfznelfzob  13933  flval  13958  fllelt  13961  flflp1  13971  flval2  13978  flval3  13979  flbi  13980  dfceil2  14003  ceilval2  14004  fleqceilz  14018  modid2  14062  addmodlteq  14113  fsequb2  14143  ssnn0fi  14152  seqf1olem2  14209  sqlecan  14377  faclbnd4lem1  14461  hashsnle1  14586  pr2pwpr  14648  hash3tpde  14662  rtrclreclem3  15239  relexpindlem  15242  sgnval  15267  sgnmulsgn  15288  01sqrexlem6  15440  01sqrex  15442  abslt  15508  absle  15509  rexanre  15540  rexico  15547  limsupgle  15670  limsupgre  15674  limsupbnd2  15676  rlim2lt  15690  rlim3  15691  ello12r  15710  ello1d  15716  elo12r  15721  rlimconst  15737  climshft  15769  rlimcn3  15783  o1rlimmul  15812  lo1le  15845  climsup  15863  caucvgrlem  15866  isumless  16040  divrcnv  16047  cvgrat  16078  rpnnen2lem10  16417  ruclem1  16425  ruclem2  16426  ruclem11  16434  ruclem12  16435  sqrt2irr  16443  absdvdsb  16470  dvdsle  16506  dvdsabseq  16509  dvdsdivcl  16512  dvdsext  16517  divalglem8  16596  divalglem9  16597  divalglem10  16598  divalgmod  16602  ndvdssub  16605  sadcaddlem  16653  gcdcllem1  16695  gcdcllem2  16696  gcdcllem3  16697  dfgcd2  16745  gcdzeq  16751  dvdssq  16768  nn0seqcvgd  16771  algcvgblem  16778  lcmval  16793  lcmdvds  16809  lcmgcdeq  16813  lcmfpr  16828  lcmf  16834  lcmftp  16837  lcmfunsnlem1  16838  lcmfunsnlem2lem1  16839  lcmfunsnlem2lem2  16840  lcmfdvdsb  16844  coprmgcdb  16850  coprmdvds1  16853  1nprm  16880  1idssfct  16881  isprm2lem  16882  isprm2  16883  dvdsprime  16888  nprm  16889  3prm  16895  dvdsprm  16905  exprmfct  16906  isprm5  16909  maxprmfct  16911  coprm  16913  prmdvdsncoprmbd  16929  ncoprmlnprm  16930  eulerthlem2  16985  phisum  16994  odzval  16995  pythagtriplem4  17023  pc2dvds  17083  pcprmpw2  17086  pcprmpw  17087  dvdsprmpweqle  17090  oddprmdvds  17107  prmpwdvds  17108  pockthg  17110  unbenlem  17112  prmreclem4  17123  prmreclem5  17124  prmreclem6  17125  1arith  17131  vdwlem6  17190  vdwlem11  17195  vdwlem13  17197  ramtlecl  17204  ramub  17217  rami  17219  ramubcl  17222  0ram  17224  ram0  17226  prmdvdsprmop  17247  prmolefac  17250  prmodvdslcmf  17251  prmgaplem2  17254  prmgaplcmlem1  17255  prmgaplcmlem2  17256  prmgaplem3  17257  prmgaplem4  17258  prmgaplem5  17259  prmgaplem6  17260  prmgapprmolem  17265  prmlem0  17309  prmlem1a  17310  imasaddfnlem  17726  imasvscafn  17735  imasleval  17739  prslem  18497  drsdir  18502  drsdirfi  18505  isdrs2  18506  posi  18517  posasymb  18519  pospropd  18525  pltval3  18537  plelttr  18542  pospo  18543  lubprop  18556  luble  18557  lublecllem  18558  glbprop  18569  joinval2lem  18578  joinlem  18581  meetlem  18595  meetle  18598  poslubmo  18609  posglbmo  18610  poslubd  18611  tleile  18619  latnlej  18656  isglbd  18709  lubub  18711  lubun  18715  clatleglb  18718  tsrlin  18785  letsr  18793  dirge  18803  pmtrval  19692  pmtrrn  19698  pmtrfrn  19699  pmtrrn2  19701  pmtrsn  19760  mndodcongi  19784  odeq  19791  odmulgeq  19798  gexnnod  19829  sylow1lem1  19839  pgpssslw  19855  sylow2a  19860  efgredeu  19993  efgred2  19994  gexex  20094  frgpnabllem2  20115  cyggenod  20125  dprdval  20246  dprdw  20253  dprdwd  20254  ablfacrplem  20308  ablfac1c  20314  ablfac1eu  20316  ablfaclem3  20330  omndadd  20369  abvtrivd  21116  zringlpir  21800  prmirredlem  21805  znleval  21887  frlmelbas  22089  ellspd  22135  islindf4  22171  psrbagconcl  22262  psrbagleadd1  22263  gsumbagdiaglem  22266  rhmpsrlem2  22276  psrlidm  22296  psrridm  22297  psrass1  22298  psrcom  22302  mplelbas  22325  mplmonmul  22372  ltbwe  22380  mhpmulcl  22497  psdmul  22514  coe1fsupp  22559  coe1ae0  22561  coe1mul2  22615  coe1tmmul  22623  pmatcoe1fsupp  23046  chfacffsupp  23201  chfacfscmulfsupp  23204  chfacfscmulgsum  23205  chfacfpmmulfsupp  23208  chfacfpmmulgsum  23209  ordtbas2  23536  ordtopn2  23540  ordtrest2lem  23548  pnfnei  23565  ordtt1  23724  ordthauslem  23728  2ndci  23793  2ndcsb  23794  2ndcredom  23795  2ndc1stc  23796  1stcrest  23798  2ndcctbss  23801  2ndcdisj  23802  2ndcsep  23805  lly1stc  23842  tx1stc  23996  ordthmeolem  24147  ufildom1  24272  xmetrtri2  24702  prdsxmetlem  24714  ssblex  24774  prdsbl  24837  comet  24859  stdbdxmet  24861  stdbdmopn  24864  met1stc  24867  dscmet  24918  metdstri  25198  metdscn  25203  xrhmeo  25294  bndth  25306  evth  25307  lebnumlem3  25311  pcovalg  25360  pco1  25363  pcocn  25365  pcopt  25370  pcopt2  25371  pcoass  25372  nmoleub3  25467  bcthlem5  25676  rrxfsupp  25750  minveclem4c  25773  minveclem2  25774  minveclem3b  25776  minveclem4  25780  minveclem6  25782  pmltpclem1  25796  pmltpc  25798  ovollb2lem  25836  ovolctb  25838  ovolunlem1  25845  ovoliunlem1  25850  ovoliunlem2  25851  ovoliun2  25854  ovolshftlem1  25857  ovolscalem1  25861  ovolicc1  25864  ovolicc2lem3  25867  voliunlem2  25899  voliunlem3  25900  ioombl1lem4  25909  uniioovol  25927  uniioombllem2  25931  uniioombllem3  25933  uniioombllem6  25936  volsup2  25953  ismbfd  25987  mbfsup  26012  mbflimsup  26014  itg1climres  26062  mbfi1fseqlem4  26066  itg2lr  26078  itg2leub  26082  itg2seq  26090  itg2monolem1  26098  itg2monolem3  26100  itg2mono  26101  itg2i1fseq2  26104  itg2gt0  26108  itg2cnlem1  26109  itg2cnlem2  26110  itg2cn  26111  iblss  26152  itgless  26164  ibladdlem  26167  iblabsr  26177  iblmulc2  26178  itgabs  26182  bddiblnc  26189  ditgeq1  26195  dvferm2lem  26333  rolle  26337  dvlip2  26342  c1liplem1  26343  c1lip1  26344  dvfsumlem2  26374  dvfsumlem4  26376  mdegleb  26409  degltlem1  26417  plyco0  26537  plyeq0lem  26556  coeeq2  26588  dgrle  26589  dgradd2  26614  plydiveu  26646  aareccl  26680  aalioulem2  26687  aaliou3lem7  26703  psercnlem1  26779  pilem2  26806  pilem3  26807  logltb  26955  divlogrlim  26990  logcnlem3  26999  cxpaddlelem  27106  rlimcnp  27320  cxplim  27326  cxploglim  27332  scvxcvx  27340  ftalem1  27427  ftalem2  27428  isppw2  27469  vmappw  27470  sgmnncl  27501  sqff1o  27536  fsumdvdsdiaglem  27537  dvdsppwf1o  27540  dvdsflsumcom  27542  musum  27545  muinv  27547  mpodvdsmulf1o  27548  dvdsmulf1o  27550  vmalelog  27559  vmasum  27570  logfac2  27571  perfectlem2  27584  bcmono  27631  bpos1lem  27636  bposlem9  27646  lgsmod  27677  lgsne0  27689  gausslemma2dlem4  27723  2sqlem6  27777  2sqlem8  27780  2sqlem10  27782  2sqreulem1  27800  2sqreunnlem1  27803  chtppilim  27829  rpvmasumlem  27841  dchrisumlema  27842  dchrisumlem2  27844  dchrvmasumlem1  27849  dchrvmasumiflem1  27855  dchrisum0flblem1  27862  dchrisum0flblem2  27863  dchrisum0  27874  rplogsum  27881  logsqvma  27896  pntpbnd1  27940  pntpbnd2  27941  pntibndlem3  27946  pntlemj  27957  pntlemi  27958  pntlem3  27963  pnt3  27966  ostth3  27992  flt4lem2  28004  flt4lem7  28016  nodense  28076  noresle  28081  nosupprefixmo  28084  noinfprefixmo  28085  nosupcbv  28086  nosupdm  28088  nosupbnd1lem1  28092  nosupbnd1lem4  28095  nosupbnd1  28098  nosupbnd2lem1  28099  nosupbnd2  28100  noinfcbv  28101  noinfdm  28103  noinffv  28105  noinfres  28106  noinfbnd1lem3  28109  noinfbnd1lem4  28110  noinfbnd1lem5  28111  noinfbnd1  28113  noetalem2  28126  nocvxminlem  28167  sltssnb  28182  sltssepc  28184  conway  28192  cutsval  28193  etaslts  28206  lesrec  28212  eqcuts3  28217  bday1  28227  cuteq1  28230  madeval2  28246  rightval  28263  elleft  28264  sltsright  28274  made0  28276  madecut  28296  left1s  28308  madebdaylemlrcut  28312  ltslpss  28321  cofslts  28331  coinitslts  28332  cofcutr  28337  cofcutrtime  28340  cofss  28343  coiniss  28344  cutmax  28347  cutmin  28348  cutminmax  28349  addsproplem1  28382  addsprop  28389  leadds1  28402  addsuniflem  28414  negsproplem1  28441  negsprop  28448  negsid  28454  negsunif  28468  mulsproplemcbv  28528  mulsproplem1  28529  mulsproplem9  28537  mulsprop  28543  sltmuls1  28560  sltmuls2  28561  mulsuniflem  28562  precsexlem11  28630  abslts  28662  oncutlt  28677  oniso  28684  bdayons  28689  addonbday  28692  n0fincut  28768  onsfi  28769  n0subs  28776  bdayn0p1  28782  eucliddivs  28789  zcuts  28820  twocut  28836  halfcut  28871  addhalfcut  28872  bdaypw2n0bndlem  28876  bdayfinbndcbv  28879  bdayfinbndlem1  28880  bdayfinbndlem2  28881  z12bdaylem1  28883  elreno  28904  elreno2  28908  tgjustc1  28964  tgjustc2  28965  iscgrglt  29004  tgcgr4  29021  hlcgreu  29111  elplng  29285  plngcplem  29290  lmif  29317  islmib  29319  trgcopyeu  29340  iscgrad  29345  inaghl  29391  axlowdim2  29565  axlowdim  29566  axcontlem2  29570  axcontlem3  29571  axcontlem4  29572  axcontlem7  29575  axcontlem9  29577  axcontlem10  29578  axcontlem11  29579  axcontlem12  29580  ebtwntg  29587  umgrupgr  29708  nbusgrvtxm1  29987  crctcshwlkn0lem2  30427  crctcshwlkn0lem3  30428  crctcsh  30440  wlkswwlksf1o  30495  clwlkclwwlklem2fv1  30613  clwlkclwwlkf  30626  0clwlkv  30749  loop1cycl  30771  umgr2cycl  30774  acycgrcycl  30780  eupth2  30867  numclwwlk5  31016  nmoubi  31401  minvecolem2  31504  minvecolem3  31505  minvecolem4c  31508  minvecolem4  31509  minvecolem5  31510  minvecolem6  31511  htthlem  31546  chlimi  31863  chcompl  31871  hsn0elch  31877  cmbr3  32237  cmcm  32243  cmcm3  32244  lecm  32246  nmopub  32537  nmfnleub  32554  nmopun  32643  nmcexi  32655  cnlnadjlem7  32702  pjnmopi  32777  stle0i  32868  stlesi  32870  stm1i  32872  csmdsymi  32963  cvmd  32965  atcveq0  32977  atcv1  33009  atord  33017  atcvat2  33018  chirred  33024  mdsym  33041  mddmdin0i  33060  cdj1i  33062  fmptcof2  33320  fnpreimac  33333  isoun  33363  fcobijfs  33380  fcobijfs2  33381  lt2addrd  33409  xlt2addrd  33418  xrge0infss  33419  infxrge0glb  33424  xrofsup  33426  fz1nnct  33460  toslublem  33600  tosglblem  33602  ismntd  33612  mgccole1  33618  mgccole2  33619  mgcmnt1  33620  mgcmnt2  33621  dfmgc2lem  33623  dfmgc2  33624  psgnfzto1stlem  33728  fzto1st  33731  psgnfzto1st  33733  trsp2cyc  33751  xrnarchi  33812  archirng  33816  archiexdiv  33818  archiabl  33826  isarchiofld  33827  elrgspnlem1  33870  elrgspnlem2  33871  elrgspnlem3  33872  elrgspnlem4  33873  elrgspn  33874  elrgspnsubrunlem1  33875  elrgspnsubrunlem2  33876  elrgspnsubrun  33877  linds2eq  34003  elrspunidl  34045  elrspunsn  34046  isrprm  34116  evl1deg1  34175  evl1deg2  34176  evl1deg3  34177  0mplrim  34213  selvply1rhmlema  34217  selvply1rhmlemb  34218  selvply1rhmlem1  34219  selvply1rhmlem2  34220  selvply1rhmlem4  34222  selvply1rhm0  34225  extvfvvcl  34234  extvfvcl  34235  mplmulmvr  34238  evlextv  34241  mplvrpmlem  34242  mplvrpmfgalem  34243  mplvrpmga  34244  mplvrpmmhm  34245  mplvrpmrhm  34246  psrmonmul  34249  psrmonprod  34251  esplyfval0  34263  esplylem  34265  esplyfv1  34268  esplyfval3  34271  esplyfvaln  34273  esplyind  34274  ply1degltdimlem  34321  lbsdiflsp0  34325  fedgmullem1  34328  fedgmullem2  34329  fedgmul  34330  fldextrspunlsplem  34372  fldextrspunlsp  34373  smatrcl  34495  smatlem  34496  madjusmdetlem2  34527  madjusmdet  34530  cmpcref  34549  ldlfcntref  34553  dispcmp  34558  zarcmplem  34580  ordtrest2NEWlem  34621  ordtconnlem1  34623  xrge0iifiso  34634  rge0scvg  34648  gsumesum  34758  esumfsup  34769  esumpinfval  34772  esumpcvgval  34777  esumcvg  34785  sigaclcu  34816  sigaclci  34831  unelsiga  34833  unelldsys  34858  sigapildsys  34862  ldgenpisyslem1  34863  fiunelros  34874  measvun  34909  voliune  34929  volfiniune  34930  oms0  34996  omssubaddlem  34998  omssubadd  34999  carsgsigalem  35014  carsgclctunlem2  35018  carsgclctun  35020  pmeasmono  35023  pmeasadd  35024  orvcval2  35158  dstfrvel  35173  ballotlemfc0  35192  ballotlemfcc  35193  ballotlemsv  35209  ballotlemsf1o  35213  breprexp  35329  tgoldbachgt  35359  bnj23  35416  bnj1185  35490  bnj1152  35695  bnj1418  35737  soinfdom  35797  fnrelpredd  35801  rankse  35822  erscottd  35842  dfac16  35845  weexenwe  35847  kardval2  35920  elkarden  35922  kardeng  35924  kardnnfi  35936  rankkardu  35938  onprcf1of1orbd  36053  dfdm5  36714  dfrn5  36715  wzel  36763  wsuclem  36764  brpprod  36824  brsset  36828  brbigcup  36837  dffix2  36844  elfuns  36854  brimageg  36866  brdomaing  36874  brrangeg  36875  brimg  36876  brapply  36877  lemsuccf  36880  funpartlem  36883  brrestrict  36890  dfrecs2  36891  dfrdg4  36892  brofs  36947  btwncomim  36955  btwnintr  36961  btwnexch3  36962  btwnexch2  36965  brifs  36985  brcolinear2  37000  colineardim1  37003  brfs  37021  btwnconn1  37043  segcon2  37047  seglerflx  37054  seglemin  37055  btwnsegle  37059  colinbtwnle  37060  broutsideof2  37064  fvray  37083  lineunray  37089  lineelsb2  37090  linerflx1  37091  trer  37281  elicc3  37282  finminlem  37283  nn0prpwlem  37287  nn0prpw  37288  fnessref  37322  refssfne  37323  weiunlem  37428  weiunfrlem  37429  weiunfr  37432  weiunse  37433  unblimceq0lem  37549  unblimceq0  37550  unbdqndv2  37554  knoppndvlem21  37575  coi1res  38150  taupilemrplb  38432  dfgcd3  38436  icorempo  38465  icoreval  38467  iooelexlt  38476  relowlssretop  38477  domalom  38518  ctbssinf  38520  pibt2  38531  phpreu  38718  fin2solem  38720  fin2so  38721  ltflcei  38722  ptrecube  38729  poimirlem1  38730  poimirlem2  38731  poimirlem5  38734  poimirlem6  38735  poimirlem7  38736  poimirlem9  38738  poimirlem12  38741  poimirlem22  38751  poimirlem23  38752  poimirlem24  38753  poimirlem26  38755  poimirlem27  38756  poimirlem32  38761  heicant  38764  mblfinlem1  38766  mblfinlem2  38767  itg2addnclem  38780  itg2addnclem3  38782  itg2addnc  38783  itg2gt0cn  38784  ibladdnclem  38785  iblmulc2nc  38794  itgabsnc  38798  ftc1anclem5  38806  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  indexdom  38859  filbcmb  38865  fdc  38870  prdsbnd  38918  heiborlem3  38938  rrnequiv  38960  rngoueqz  39065  eqbrtr  39361  elrnressn  39403  inxprnres  39421  presucmap  39618  eqvreltr  39814  prtlem10  40113  lsatcveq0  40280  lsatcv1  40296  oposlem  40430  opnlen0  40436  lub0N  40437  glb0N  40441  omllaw  40491  cmtbr4N  40503  cvrval  40517  cvrnbtwn  40519  cvrnbtwn2  40523  cvrnbtwn3  40524  cvrcon3b  40525  cvrnbtwn4  40527  atcvreq0  40562  atnle  40565  atlatmstc  40567  cvlexch1  40576  glbconN  40625  hlsuprexch  40629  exatleN  40652  cvratlem  40669  atcvrj0  40676  atcvrj2b  40680  atlelt  40686  cvrat4  40691  3dim1lem5  40714  3dim2  40716  3dim3  40717  ps-2  40726  llni  40756  llnn0  40764  llnle  40766  lplni  40780  lplni2  40785  lplnle  40788  lplnn0N  40795  llncvrlpln  40806  2llnjN  40815  lvoli  40823  lvoli3  40825  lvoli2  40829  lvoln0N  40839  4at  40861  lplncvrlvol  40864  2lplnj  40868  dalemcea  40908  dalem3  40912  psubspi  40995  linepsubN  41000  elpmap  41006  pmapsub  41016  lnatexN  41027  cdlema1N  41039  cdlemb  41042  elpadd  41047  paddvaln0N  41049  paddasslem5  41072  llnexchb2lem  41116  llnexch2N  41118  islhp  41244  lhpat3  41294  4atexlemex2  41319  4atex  41324  4atex2-0aOLDN  41326  4atex2-0cOLDN  41328  lautle  41332  lautcvr  41340  lauteq  41343  ldilval  41361  ltrnu  41369  trlval2  41411  trlne  41433  cdleme0ex1N  41471  cdleme0nex  41538  cdleme18d  41543  cdlemednuN  41548  cdleme25b  41602  cdleme25cv  41606  cdleme27b  41616  cdleme29b  41623  cdleme31sn  41628  cdleme31fv  41638  cdleme31fv2  41641  cdlemefrs29bpre0  41644  cdlemefr29bpre0N  41654  cdlemefr29clN  41655  cdlemefr32fvaN  41657  cdlemefr32fva1  41658  cdlemefs29pre00N  41660  cdlemefs32sn1aw  41662  cdlemefs29bpre0N  41664  cdlemefs29bpre1N  41665  cdlemefs29cpre1N  41666  cdlemefs29clN  41667  cdlemefs32fvaN  41670  cdlemefs32fva1  41671  cdleme41sn3a  41681  cdleme32fva  41685  cdleme32e  41693  cdleme35f  41702  cdleme40v  41717  cdleme42b  41726  trlord  41817  cdlemg1cex  41836  diaval  42280  diaeldm  42284  diaelrnN  42293  cdlemm10N  42366  dibglbN  42414  dicval  42424  dicfnN  42431  dicvalrelN  42433  dihval  42480  dihlsscpre  42482  dihglblem3N  42543  dihmeetlem2N  42547  djhcvat42  42663  lcmineqlem4  43273  aks4d1p4  43320  aks4d1p5  43321  aks4d1p7  43324  aks4d1p8d2  43326  aks4d1p8  43328  hashnexinjle  43370  sticksstones1  43387  sticksstones2  43388  sticksstones10  43396  sticksstones12a  43398  aks6d1c7lem4  43424  aks6d1c7  43425  grpods  43435  unitscyglem2  43437  unitscyglem3  43438  unitscyglem4  43439  qsalrel  43483  supinf  43484  dvdsexpnn0  43577  redvmptabs  43602  sn-nnne0  43715  sn-sup2  43746  fimgmcyclem  43788  lzenom  43972  fphpdo  44015  irrapxlem4  44023  pellexlem6  44032  infmrgelbi  44076  pellfundre  44079  pellfundlb  44082  monotoddzz  44141  zindbi  44144  jm2.27  44206  rmydioph  44212  rpnnen3lem  44229  aomclem8  44254  hbtlem5  44320  hbt  44322  sdomne0  44604  sdomne0d  44605  ensucne0  44720  sucomisnotcard  44735  en2pr  44738  pr2cv  44739  refimssco  44797  rfovfvfvd  45193  rfovcnvf1od  45194  fsovrfovd  45199  nzss  45491  relprel  46134  permaxinf2lem  46195  wessf1ornlem  46403  axccdom  46438  dmrelrnrel  46442  axccd  46444  rnmptlb  46458  rnmptbdd  46460  rnmptbd2  46464  rnmptbdlem  46470  rnmptbd  46471  dstregt0  46501  suplesup  46554  supxrunb3  46613  supxrleubrnmpt  46619  rexabslelem  46631  rexabsle  46632  suprleubrnmpt  46635  infrnmptle  46636  infxrunb3rnmpt  46641  infxrpnf  46659  supminfxr  46677  infrpgernmpt  46678  xrpnf  46698  limsupre  46854  limsupref  46898  limsupbnd1f  46899  limsuppnfd  46915  climinf2  46920  limsuppnf  46924  climinfmpt  46928  climinf3  46929  limsupmnflem  46933  limsupmnf  46934  limsupre2  46938  limsupmnfuzlem  46939  limsupre2mpt  46943  limsupre3lem  46945  limsupre3  46946  limsupre3mpt  46947  limsupre3uzlem  46948  limsupre3uz  46949  limsupreuz  46950  limsupreuzmpt  46952  liminfval2  46981  liminfreuzlem  47015  liminfreuz  47016  xlimpnfxnegmnf  47027  cnrefiisplem  47042  xlimpnfv  47051  xlimpnf  47055  xlimpnfmpt  47057  dfxlim2  47061  icccncfext  47100  cncficcgt0  47101  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  stoweidlem5  47218  stoweidlem20  47233  stoweidlem26  47239  stoweidlem28  47241  stoweidlem29  47242  stoweidlem34  47247  wallispilem3  47280  stirlinglem13  47299  fourierdlem41  47361  fourierdlem42  47362  fourierdlem51  47370  fourierdlem54  47373  salunicl  47529  saluncl  47530  salexct  47547  salexct2  47552  salexct3  47555  salgencntex  47556  salgensscntex  47557  sge0pnffigt  47609  meadjuni  47670  omeunile  47718  ovnlerp  47775  hoidifhspval  47821  ovolval5lem2  47866  salpreimagelt  47920  pimincfltioo  47931  salpreimagtge  47938  salpreimagtlt  47943  incsmf  47955  issmfgt  47969  smfpreimagt  47975  decsmf  47980  issmfge  47983  smfpimgtxr  47993  smfpreimage  47995  smfinflem  48030  smfinf  48031  finfdm  48059  funressnfv  48316  funressnvmo  48318  funressnmo  48319  dfdfat2  48401  tz6.12-afv  48446  funressndmafv2rn  48496  tz6.12-afv2  48513  dfatcolem  48528  dfatco  48529  zplusmodne  48622  m1modne  48627  minusmod5ne  48628  submodneaddmod  48630  modmknepk  48641  iccpartigtl  48708  iccpartgt  48712  icceuelpartlem  48720  iccpartnel  48723  sprsymrelfolem2  48778  nprmmul2  48813  goldbachthlem2  48834  odz2prm2pw  48851  fmtnoprmfac1  48853  fmtnoprmfac2  48855  fmtnofac2  48857  fmtno4prmfac  48860  fmtno4prm  48863  prmdvdsfmtnof1lem1  48872  31prm  48885  nprmdvdsfacm1  48912  perfectALTVlem2  49023  nnsum3primes4  49089  nnsum3primesprm  49091  nnsum3primesgbe  49093  nnsum3primesle9  49095  nnsum4primeseven  49101  nnsum4primesevenALTV  49102  wtgoldbnnsum4prm  49103  bgoldbnnsum3prm  49105  bgoldbtbndlem4  49109  bgoldbtbnd  49110  tgblthelfgott  49116  tgoldbach  49118  assintop  49509  isassintop  49510  assintopcllaw  49512  ztprmneprm  49662  ply1mulgsumlem1  49701  ply1mulgsumlem2  49702  lco0  49742  lcoel0  49743  lincsumcl  49746  lincscmcl  49747  lcoss  49751  linindslinci  49763  lindslinindsimp1  49772  linds0  49780  el0ldep  49781  lindsrng01  49783  ldepspr  49788  islindeps2  49798  isldepslvec2  49800  zlmodzxzldep  49819  ldepsnlinc  49823  elbigo2r  49868  xpco2  50171  tposres0  50193  lubsscl  50277  glbsscl  50278  lubprlem  50279  ipolub  50305  ipoglb  50308  catprslem  50327  infsubc2  50378  nelsubc3lem  50387  cnelsubcw  50944