Theorem ralbidv 3178

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 482	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3176	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  2ralbidv  3219  rexralbidv  3221  3ralbidv  3222  4ralbidv  3223  cbvral2vw  3239  cbvral4vw  3242  cbvral2v  3365  rspceaimv  3618  rspc2  3621  rspc2v  3623  rspc3v  3628  rspc4v  3631  reu6i  3725  reu7  3729  sbcralt  3867  reu8nf  3872  raaan  4521  raaanv  4522  raaan2  4525  2reu4lem  4526  reusngf  4677  2ralsng  4681  rexreusng  4684  reuprg0  4707  issn  4834  2ralunsn  4896  elintg  4959  elintrabg  4966  eliin  5003  disjprgw  5144  disjprg  5145  disjxun  5147  brralrspcev  5209  reusv2lem2  5398  reusv3  5404  poeq1  5592  solin  5614  somo  5626  frirr  5654  fr2nr  5655  frminex  5657  wereu2  5674  posn  5762  frsn  5764  ralxpf  5847  cnvpo  6287  reu3op  6292  reuop  6293  dfpo2  6296  frpomin  6342  fnmptfvd  7043  iinpreima  7071  dff4  7103  dff13f  7255  fpropnf1  7266  eusvobj2  7401  ovanraleqv  7433  f1opr  7465  ofreq  7674  sorpssuni  7722  sorpssint  7723  fr3nr  7759  onssmin  7780  funcnvuni  7922  f1oweALT  7959  frxp  8112  frxp2  8130  xpord2indlem  8133  frxp3  8137  xpord3inddlem  8140  poseq  8144  soseq  8145  frecseq123  8267  csbfrecsg  8269  frrlem1  8271  frrlem13  8283  wrecseq123OLD  8300  wfrlem1OLD  8308  wfrlem3OLDa  8311  wfrlem15OLD  8323  smoeq  8350  tfrlem12  8389  tz7.48lem  8441  naddcllem  8675  naddov2  8678  naddunif  8692  naddasslem1  8693  naddasslem2  8694  elixp2  8895  undifixp  8928  xpf1o  9139  nneneq  9209  nneneqOLD  9221  ac6sfi  9287  frfi  9288  fipreima  9358  indexfi  9360  marypha1lem  9428  marypha1  9429  supeq1  9440  supeq3  9444  supmo  9447  eqsup  9451  supub  9454  suplub  9455  sup0  9461  supisoex  9469  eqinf  9479  infval  9481  infmo  9490  oieq1  9507  ordtypecbv  9512  ordtypelem3  9515  ordtypelem6  9518  ordtypelem7  9519  ordtypelem9  9521  wemaplem1  9541  wemaplem2  9542  zfregcl  9589  oemapval  9678  oemapvali  9679  cantnf  9688  wemapwe  9692  ttrcleq  9704  ttrcltr  9711  ttrclss  9715  ttrclselem2  9721  rankval3b  9821  unbndrank  9837  rankunb  9845  rankuni2b  9848  tcrank  9879  scottex  9880  scottexs  9882  scott0s  9883  bnd2  9888  updjud  9929  dfac8clem  10027  ac5num  10031  acni  10040  acni2  10041  alephval3  10105  dfac4  10117  dfac5lem5  10122  dfac5  10123  dfac2a  10124  dfac2b  10125  dfacacn  10136  kmlem2  10146  kmlem13  10157  cflem  10241  cflecard  10248  cfeq0  10251  cfsuc  10252  cfflb  10254  cofsmo  10264  cfsmolem  10265  cfcoflem  10267  coftr  10268  alephsing  10271  fin23lem11  10312  isfin3ds  10324  fin23lem17  10333  fin23lem39  10345  isf33lem  10361  isf34lem6  10375  fin1a2lem13  10407  hsmexlem4  10424  hsmex  10427  axcc2lem  10431  axcc3  10433  dcomex  10442  axdc2lem  10443  axdc3lem2  10446  axdc3lem3  10447  axdc3  10449  axdc4lem  10450  axcclem  10452  zorn2lem2  10492  zorn2lem7  10497  zorn2g  10498  zornn0g  10500  ttukeylem7  10510  axdclem2  10515  brdom3  10523  brdom7disj  10526  brdom6disj  10527  alephval2  10567  inar1  10770  axgroth6  10823  pinq  10922  nqereu  10924  prlem934  11028  supexpr  11049  supsrlem  11106  axpre-sup  11164  dedekind  11377  dedekindle  11378  fiminre2  12162  lbreu  12164  sup2  12170  infm3  12173  nnsub  12256  uzwo  12895  nnwof  12898  ublbneg  12917  lbzbi  12920  zsupss  12921  uzsupss  12924  uzwo3  12927  zmax  12929  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem4  12964  rpnnen1lem5  12965  xrsupsslem  13286  xrinfmsslem  13287  xrsupss  13288  xrinfmss  13289  flval2  13779  axdc4uzlem  13948  ssnn0fi  13950  fsuppmapnn0fiubex  13957  faclbnd4lem4  14256  bccl  14282  hashgt12el  14382  hashbc  14412  hashge2el2dif  14441  wrdind  14672  wrd2ind  14673  rexanre  15293  rexico  15300  cau4  15303  reusq0  15409  clim  15438  rlim  15439  rlim2  15440  clim2  15448  clim2c  15449  clim0c  15451  rlim0  15452  rlim0lt  15453  ello12r  15461  ello1d  15467  elo12r  15472  rlimresb  15509  rlimcld2  15522  climabs0  15529  rlimo1  15561  lo1add  15571  lo1mul  15572  isercoll  15614  incexclem  15782  sqrt2irr  16192  gcdcllem1  16440  gcdcllem2  16441  dfgcd2  16488  fissn0dvds  16556  dvdslcmf  16568  lcmfledvds  16569  lcmf  16570  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem  16578  lcmfdvds  16579  reumodprminv  16737  pc2dvds  16812  pcz  16814  prmpwdvds  16837  infpn2  16846  prmreclem2  16850  prmreclem3  16851  prmreclem5  16853  prmreclem6  16854  vdwlem6  16919  vdwlem8  16921  vdwlem13  16926  vdwnnlem1  16928  vdwnn  16931  ramcl  16962  cshwrepswhash1  17036  prdsleval  17423  imasval  17457  imasaddfnlem  17474  imasvscafn  17483  mrisval  17574  isacs  17595  isacs2  17597  isacs1i  17601  mreacs  17602  acsfn  17603  acsfn2  17607  iscatd  17617  catidex  17618  catideu  17619  cidval  17621  catidd  17624  comfeq  17650  catpropd  17653  ismon  17680  isfunc  17814  isnat  17898  isinito  17946  istermo  17947  isprs  18250  drsdirfi  18258  ispos  18267  lubfval  18303  lubeldm  18306  lubval  18309  lubprop  18311  lublecllem  18313  glbfval  18316  glbeldm  18319  glbval  18322  glbprop  18324  joinval2lem  18333  joinlem  18336  meetval2lem  18347  meetlem  18350  poslubmo  18364  posglbmo  18365  poslubd  18366  isglbd  18462  lubl  18465  lubun  18468  clatleglb  18471  isdlat  18475  ipodrsima  18494  mgm1  18577  gsumval2  18605  sgrp1  18620  mhmimalem  18705  mndind  18709  gsumwspan  18727  efmndmnd  18770  smndex1mnd  18791  sgrp2rid2  18807  sgrp2rid2ex  18808  sgrp2nmndlem4  18809  pwmnd  18818  dfgrp2  18847  isgrpinv  18878  grpidinv  18883  dfgrp3lem  18921  issubg4  19025  0subgOLD  19032  isnsg2  19036  nsgacs  19042  elnmz  19043  cycsubgcl  19083  ghmrn  19105  ghmnsgima  19116  isga  19155  orbsta  19177  cntzfval  19184  elcntz  19186  resscntz  19197  oppgsubg  19230  symgextfo  19290  gsmsymgreqlem2  19299  gsmsymgreq  19300  pmtrdifel  19348  pmtrdifwrdellem3  19351  pmtrdifwrdel2  19354  psgnunilem2  19363  psgnunilem3  19364  odeq  19418  gexid  19449  gexlem2  19450  gexdvds  19452  isslw  19476  sylow2alem1  19485  sylow2alem2  19486  efgval  19585  efgrelexlemb  19618  efgcpbllemb  19623  abl1  19734  dmdprd  19868  dprd2da  19912  pgpfac1lem5  19949  ring1  20122  lringuplu  20314  isabv  20427  islss  20545  lssacs  20578  reslmhm  20663  islbs  20687  pj1lmhm  20711  lbsacsbs  20769  isrrg  20904  zringlpir  21037  psgndiflemA  21154  ocvfval  21219  elocv  21221  iunocv  21234  frlmlbs  21352  islindf  21367  islinds2  21368  islindf2  21369  lindfrn  21376  lsslindf  21385  islindf4  21393  opsrval  21601  ply1coe  21820  cply1coe0bi  21824  mat0dimcrng  21972  mdetunilem1  22114  mdetunilem9  22122  cpmat  22211  cpmatel  22213  1elcpmat  22217  m2cpminvid2lem  22256  basgen2  22492  bastop1  22496  isclo  22591  ordtbaslem  22692  iscn  22739  cnpval  22740  iscnp  22741  iscnp3  22748  lmbr  22762  lmbr2  22763  lmbrf  22764  cnprest  22793  cnprest2  22794  t0sep  22828  isreg  22836  t1sep2  22873  tgcmp  22905  1stcclb  22948  1stcfb  22949  2ndc1stc  22955  1stcrest  22957  2ndcdisj  22960  islly  22972  isnlly  22973  lly1stc  23000  isref  23013  islocfin  23021  elkgen  23040  kgencn  23060  elpt  23076  elptr  23077  ptcnplem  23125  tx1stc  23154  cnmpt21  23175  kqt0lem  23240  isr0  23241  regr1lem2  23244  r0sep  23252  nrmr0reg  23253  flffbas  23499  cnflf  23506  cnflf2  23507  lmflf  23509  txflf  23510  fclsopni  23519  fclsnei  23523  fclsrest  23528  fcfnei  23539  cnfcf  23546  alexsubb  23550  alexsubALTlem3  23553  qustgplem  23625  tsmsfbas  23632  tsmsres  23648  tsmsf1o  23649  tsmsxplem1  23657  ustval  23707  isust  23708  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  ust0  23724  utopval  23737  ucnval  23782  isucn  23783  isucn2  23784  ucnima  23786  iscfilu  23793  ispsmet  23810  ismet  23829  isxmet  23830  imasdsf1olem  23879  imasf1oxmet  23881  imasf1omet  23882  metss  24017  met1stc  24030  prdsxmslem2  24038  txmetcnp  24056  metucn  24080  tngngp3  24173  nlmvscn  24204  nmoval  24232  nmolb  24234  qtopbaslem  24275  cncfval  24404  elcncf2  24406  mulc1cncf  24421  cncfmet  24425  evth  24475  lebnumlem3  24479  lebnum  24480  xlebnum  24481  ishtpy  24488  isphtpy  24497  pi1xfr  24571  pi1coghm  24577  isclmp  24613  ipcn  24763  lmmbr2  24776  lmmbr3  24777  lmmbrf  24779  cfilfval  24781  iscfil  24782  fmcfil  24789  caufval  24792  iscau  24793  iscau2  24794  iscau3  24795  iscau4  24796  iscauf  24797  caucfil  24800  cfilresi  24812  causs  24815  lmclim  24820  cmetcusp1  24870  minveclem4c  24942  minveclem2  24943  minveclem3b  24945  minveclem4  24949  minveclem6  24951  minveclem7  24952  ovolicc2lem3  25036  ismbl  25043  dyadmax  25115  dyadmbllem  25116  dyadmbl  25117  opnmbllem  25118  ismbf1  25141  ismbf  25145  mbfeqalem2  25159  mbflimsup  25183  mbfi1fseqlem6  25238  mbfi1flimlem  25240  itg2seq  25260  itg2monolem1  25268  isibl  25283  ply1divex  25654  fta1g  25685  dgrco  25789  plydivex  25810  fta1  25821  vieta1  25825  aannenlem1  25841  aannenlem2  25842  aalioulem2  25846  aalioulem3  25847  ulmval  25892  ulm2  25897  ulmi  25898  ulmres  25900  ulmshftlem  25901  ulmcaulem  25906  ulmcau  25907  ulmss  25909  ulmbdd  25910  ulmdvlem1  25912  ulmdvlem3  25914  pilem2  25964  pilem3  25965  cxpcn3  26256  dmarea  26462  rlimcnp  26470  scvxcvx  26490  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem5  26537  lgambdd  26541  lgamcvglem  26544  isppw2  26619  perfectlem2  26733  2sqlem6  26926  2sqlem10  26931  addsq2reu  26943  2sqreulem1  26949  2sqreunnlem1  26952  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  pntpbnd  27091  pntibndlem3  27095  pntibnd  27096  pntleme  27111  pntlem3  27112  pntlemp  27113  pnt3  27115  sltval  27150  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupno  27206  nosupdm  27207  nosupfv  27209  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1lem3  27213  nosupbnd1lem5  27215  noinfcbv  27220  noinfno  27221  noinfdm  27222  noinffv  27224  noinfres  27225  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noetalem1  27244  noetalem2  27245  nocvxminlem  27279  brsslt  27287  conway  27300  etasslt  27314  slerec  27320  madebdaylemlrcut  27393  madebday  27394  cofcutr  27411  lrrecfr  27427  addsprop  27460  negsunif  27529  istrkgld  27710  axtg5seg  27716  tgcgr4  27782  perpln1  27961  perpln2  27962  isperp  27963  brbtwn2  28163  colinearalg  28168  axsegconlem1  28175  axsegcon  28185  ax5seglem4  28190  ax5seglem5  28191  axlowdim  28219  axeuclidlem  28220  axcontlem1  28222  axcontlem2  28223  axcontlem4  28225  axcontlem5  28226  axcontlem8  28229  axcontlem12  28233  elntg2  28243  uvtxusgr  28659  rgrx0ndm  28850  ewlksfval  28858  wksfval  28866  wwlks  29089  wlkiswwlks2  29129  clwwlk  29236  1conngr  29447  frgrwopregasn  29569  frgrwopregbsn  29570  frgrwopreglem5ALT  29575  frgrregord013  29648  isgrpo  29750  isgrpoi  29751  grpoideu  29762  grpoidinv2  29768  vciOLD  29814  isvclem  29830  cnidOLD  29835  isnvlem  29863  nvi  29867  lnoval  30005  islno  30006  isblo3i  30054  blo3i  30055  blocnilem  30057  ajfval  30062  ubthlem1  30123  ubthlem2  30124  ubthlem3  30125  ubth  30126  minvecolem2  30128  minvecolem3  30129  minvecolem4c  30132  minvecolem4  30133  minvecolem5  30134  minvecolem6  30135  minvecolem7  30136  h2hcau  30232  h2hlm  30233  hilid  30414  hcau  30437  hlimi  30441  hlim2  30445  ocel  30534  adjsym  31086  ellnop  31111  ellnfn  31136  hhcno  31157  hhcnf  31158  lnopeq  31262  elunop2  31266  lnophm  31272  lnconi  31286  lnopcnbd  31289  lnfncnbd  31310  imaelshi  31311  riesz3i  31315  riesz4i  31316  riesz4  31317  riesz1  31318  cnlnadjlem2  31321  cnlnadjlem5  31324  cnlnadjlem8  31327  cnlnadji  31329  nmopadjlei  31341  cnvbraval  31363  leopg  31375  leoppos  31379  mdbr  31547  dmdbr  31552  cdj3i  31694  disjunsn  31825  funcnv5mpt  31893  fgreu  31897  fcnvgreu  31898  xrge0infss  31973  wrdt2ind  32117  resspos  32136  mgccole1  32160  mgccole2  32161  mgcmnt1  32162  mgcmnt2  32163  gsumhashmul  32208  isomnd  32219  inftmrel  32326  isinftm  32327  archiabl  32344  isarchiofld  32435  0nellinds  32483  lindssn  32494  elrspunidl  32546  prmidl  32558  ismxidl  32578  crefeq  32825  zarcmplem  32861  esum2d  33091  sigaval  33109  issgon  33121  isrnmeas  33198  ismbfm  33249  mbfmcst  33258  elcarsg  33304  sitgval  33331  eulerpartlemd  33365  ballotleme  33495  tgoldbachgt  33675  bnj1185  33804  bnj1385  33843  bnj66  33871  bnj106  33879  bnj155  33890  bnj852  33932  bnj893  33939  bnj1228  34022  bnj1234  34024  bnj1463  34066  nummin  34094  derangenlem  34162  subfacp1lem3  34173  subfacp1lem5  34175  subfacp1lem6  34176  subfacp1  34177  erdszelem8  34189  kur14  34207  cnpconn  34221  resconn  34237  cvmscbv  34249  iscvm  34250  cvmsi  34256  cvmsval  34257  cvmlift3lem2  34311  snmlval  34322  satfv1  34354  fmlasucdisj  34390  satffunlem1lem1  34393  satffunlem2lem1  34395  satfv1fvfmla1  34414  mclsssvlem  34553  mclsval  34554  mclsax  34560  mclsind  34561  dfon2lem9  34763  dfrdg2  34767  dfrdg3  34768  fwddifnval  35135  nn0prpwlem  35207  isfne  35224  isfne4  35225  isfne2  35227  isfne3  35228  neibastop3  35247  topmeet  35249  topjoin  35250  filnetlem4  35266  unblimceq0lem  35382  unblimceq0  35383  unbdqndv2  35387  taupilemrplb  36201  fin2so  36475  lindsadd  36481  matunitlindflem2  36485  ptrecube  36488  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem29  36517  poimirlem30  36518  poimirlem32  36520  poimir  36521  heicant  36523  mblfinlem1  36525  mblfinlem2  36526  voliunnfl  36532  volsupnfl  36533  mbfresfi  36534  itg2addnc  36542  upixp  36597  indexdom  36602  filbcmb  36608  sdclem2  36610  fdc  36613  lmclim2  36626  caures  36628  istotbnd  36637  istotbnd3  36639  sstotbnd  36643  isbnd  36648  heibor  36689  bfp  36692  rrncmslem  36700  isgrpda  36823  idlval  36881  isidl  36882  0idl  36893  unichnidl  36899  pridl  36905  ismaxidl  36908  smprngopr  36920  igenval2  36934  prnc  36935  ispridlc  36938  scottexf  37036  scott0f  37037  disjsuc2  37261  riotasvd  37826  islfl  37930  eqlkr  37969  eqlkr3  37971  glbconN  38247  glbconNOLD  38248  hlsuprexch  38252  ispsubsp  38616  ldilset  38980  isldil  38981  dilsetN  39024  isdilN  39025  trlset  39032  trlval  39033  cdleme27b  39239  cdleme29b  39246  cdleme31so  39250  cdleme31sn1  39252  cdleme31sn1c  39259  cdleme31fv  39261  cdleme40v  39340  istendo  39631  cdlemkid3N  39804  cdlemkid4  39805  cdlemkid5  39806  dihfval  40102  dihval  40103  islpolN  40354  hdmapffval  40697  hdmapfval  40698  hdmapval  40699  hdmapval2lem  40702  hgmapffval  40756  hgmapfval  40757  hgmapval  40758  hgmapvs  40762  sticksstones2  40963  qsalrel  41062  fsuppind  41162  sn-sup2  41342  isnacs  41442  isnacs2  41444  nacsfix  41450  mzpclval  41463  elmzpcl  41464  rencldnfilem  41558  infmrgelbi  41616  pellfundre  41619  pellfundlb  41622  wepwsolem  41784  fnwe2lem2  41793  aomclem8  41803  dfac11  41804  gicabl  41841  islnr3  41857  hbtlem2  41866  hbtlem5  41870  onintunirab  41976  onsucf1lem  42019  cantnfresb  42074  safesnsupfilb  42169  rp-brsslt  42174  fiinfi  42324  clsk1independent  42797  ntrclsk13  42822  gneispacess2  42897  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2lem1  42921  imo72b2  42924  scottelrankd  43006  mnuop23d  43025  ismnushort  43060  evth2f  43699  evthf  43711  fnchoice  43713  uzwo4  43740  wessf1ornlem  43882  disjinfi  43891  rnmptlb  43947  rnmptbdd  43949  rnmptbd2  43953  rnmptbd  43960  dstregt0  43991  upbdrech2  44018  rexabslelem  44128  rexabsle  44129  uzub  44141  infrpgernmpt  44175  mccl  44314  ellimcabssub0  44333  climf  44338  clim2f  44352  limsupre  44357  clim2cf  44366  clim0cf  44370  climf2  44382  clim2f2  44386  clim2d  44389  limsupref  44401  limsupbnd1f  44402  climinf2  44423  limsuppnf  44427  climinfmpt  44431  climinf3  44432  limsupubuzmpt  44435  limsupmnf  44437  limsupre2lem  44440  limsupre2  44441  limsupmnfuzlem  44442  limsupmnfuz  44443  limsupre2mpt  44446  limsupre3lem  44448  limsupre3  44449  limsupre3mpt  44450  limsupre3uz  44452  limsupreuz  44453  limsupreuzmpt  44455  climuz  44460  liminfreuzlem  44518  liminfreuz  44519  cnrefiisplem  44545  xlimmnfvlem1  44548  xlimmnfv  44550  xlimpnfvlem1  44552  xlimpnfv  44554  xlimmnfmpt  44559  xlimpnfmpt  44560  cncfshift  44590  cncfperiod  44595  fperdvper  44635  dvbdfbdioo  44646  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem3  44664  stoweidlem5  44721  stoweidlem9  44725  stoweidlem15  44731  stoweidlem16  44732  stoweidlem27  44743  stoweidlem28  44744  stoweidlem31  44747  stoweidlem34  44750  stoweidlem37  44753  stoweidlem46  44762  stoweidlem48  44764  stoweidlem51  44767  stoweidlem52  44768  stoweidlem59  44775  wallispilem3  44783  stirlinglem13  44802  fourierdlem2  44825  fourierdlem3  44826  fourierdlem16  44839  fourierdlem20  44843  fourierdlem21  44844  fourierdlem22  44845  fourierdlem25  44848  fourierdlem39  44862  fourierdlem42  44865  fourierdlem54  44876  fourierdlem64  44886  fourierdlem77  44899  fourierdlem83  44905  fourierdlem103  44925  fourierdlem104  44926  subsaliuncllem  45073  iundjiun  45176  meaiunincf  45199  caragenval  45209  isome  45210  caragenel  45211  omessle  45214  ovnlerp  45278  hoidmvlelem3  45313  hoidmvle  45316  issmflem  45443  issmfgt  45472  smfmullem2  45508  smfmullem4  45510  smfmul  45511  smfsuplem2  45528  smfsup  45530  smfinflem  45533  smfinf  45534  fsupdm  45558  finfdm  45562  cfsetsnfsetf  45768  cbvral2  45811  2reu8i  45821  2reuimp0  45822  dfdfat2  45836  iccpart  46084  iccpartigtl  46091  paireqne  46179  reupr  46190  perfectALTVlem2  46390  bgoldbachlt  46481  tgoldbachlt  46484  isomgreqve  46493  isomushgr  46494  isomuspgrlem2  46501  isomgrsym  46504  isomgrtr  46507  ushrisomgr  46509  upwlksfval  46513  mgmhmima  46572  nn0mnd  46589  rngisomring  46719  rhmimasubrnglem  46744  rnglidlmcl  46748  rnglidl0  46752  uzlidlring  46827  ply1mulgsumlem1  47067  ply1mulgsumlem2  47068  linindslinci  47129  lindslinindsimp1  47138  lindslinindsimp2lem5  47143  lindslinindsimp2  47144  linds0  47146  lindsrng01  47149  snlindsntor  47152  lmod1  47173  ldepsnlinc  47189  bigoval  47235  elbigo2r  47239  nn0sumshdiglem2  47308  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  lubeldm2d  47591  glbeldm2d  47592  lubsscl  47593  glbsscl  47594  ipolubdm  47612  ipolub  47613  ipoglbdm  47615  ipoglb  47616  isthincd2lem2  47656  setrec1lem2  47733