Theorem ralbidv 3108

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 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3107	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3056

This theorem is referenced by:  2ralbidv  3110  rexralbidv  3210  cbvral2vw  3361  cbvral2v  3364  rspceaimv  3532  rspc2  3535  rspc2v  3537  rspc3v  3540  reu6i  3630  reu7  3634  sbcralt  3771  reu8nf  3776  raaan  4418  raaanv  4419  raaan2  4422  2reu4lem  4423  reusngf  4574  2ralsng  4578  rexreusng  4581  reuprg0  4604  issn  4729  2ralunsn  4792  elintg  4853  elintrabg  4858  eliin  4895  disjprgw  5034  disjprg  5035  disjxun  5037  brralrspcev  5099  reusv2lem2  5277  reusv3  5283  poeq1  5456  solin  5478  somo  5490  frirr  5513  fr2nr  5514  frminex  5516  wereu2  5533  posn  5619  frsn  5621  ralxpf  5700  cnvpo  6130  reu3op  6135  reuop  6136  frpomin  6172  fnmptfvd  6839  iinpreima  6867  dff4  6898  dff13f  7046  fpropnf1  7057  eusvobj2  7184  ovanraleqv  7215  f1opr  7245  ofreq  7450  sorpssuni  7498  sorpssint  7499  fr3nr  7535  onssmin  7554  funcnvuni  7687  f1oweALT  7723  frxp  7871  frecseq123  8002  frrlem1  8005  frrlem13  8017  wrecseq123  8026  wfrlem1  8032  wfrlem3a  8035  wfrlem15  8047  smoeq  8065  tfrlem12  8103  tz7.48lem  8155  elixp2  8560  undifixp  8593  xpf1o  8786  nneneq  8807  ac6sfi  8893  frfi  8894  fipreima  8960  indexfi  8962  marypha1lem  9027  marypha1  9028  supeq1  9039  supeq3  9043  supmo  9046  eqsup  9050  supub  9053  suplub  9054  sup0  9060  supisoex  9068  eqinf  9078  infval  9080  infmo  9089  oieq1  9106  ordtypecbv  9111  ordtypelem3  9114  ordtypelem6  9117  ordtypelem7  9118  ordtypelem9  9120  wemaplem1  9140  wemaplem2  9141  zfregcl  9188  oemapval  9276  oemapvali  9277  cantnf  9286  wemapwe  9290  rankval3b  9407  unbndrank  9423  rankunb  9431  rankuni2b  9434  tcrank  9465  scottex  9466  scottexs  9468  scott0s  9469  bnd2  9474  updjud  9515  dfac8clem  9611  ac5num  9615  acni  9624  acni2  9625  alephval3  9689  dfac4  9701  dfac5lem5  9706  dfac5  9707  dfac2a  9708  dfac2b  9709  dfacacn  9720  kmlem2  9730  kmlem13  9741  cflem  9825  cflecard  9832  cfeq0  9835  cfsuc  9836  cfflb  9838  cofsmo  9848  cfsmolem  9849  cfcoflem  9851  coftr  9852  alephsing  9855  fin23lem11  9896  isfin3ds  9908  fin23lem17  9917  fin23lem39  9929  isf33lem  9945  isf34lem6  9959  fin1a2lem13  9991  hsmexlem4  10008  hsmex  10011  axcc2lem  10015  axcc3  10017  dcomex  10026  axdc2lem  10027  axdc3lem2  10030  axdc3lem3  10031  axdc3  10033  axdc4lem  10034  axcclem  10036  zorn2lem2  10076  zorn2lem7  10081  zorn2g  10082  zornn0g  10084  ttukeylem7  10094  axdclem2  10099  brdom3  10107  brdom7disj  10110  brdom6disj  10111  alephval2  10151  inar1  10354  axgroth6  10407  pinq  10506  nqereu  10508  prlem934  10612  supexpr  10633  supsrlem  10690  axpre-sup  10748  dedekind  10960  dedekindle  10961  fiminre2  11745  lbreu  11747  sup2  11753  infm3  11756  nnsub  11839  uzwo  12472  nnwof  12475  ublbneg  12494  lbzbi  12497  zsupss  12498  uzsupss  12501  uzwo3  12504  zmax  12506  rpnnen1lem1  12539  rpnnen1lem3  12540  rpnnen1lem4  12541  rpnnen1lem5  12542  xrsupsslem  12862  xrinfmsslem  12863  xrsupss  12864  xrinfmss  12865  flval2  13354  axdc4uzlem  13521  ssnn0fi  13523  fsuppmapnn0fiubex  13530  faclbnd4lem4  13827  bccl  13853  hashgt12el  13954  hashbc  13982  hashge2el2dif  14011  wrdind  14252  wrd2ind  14253  rexanre  14875  rexico  14882  cau4  14885  reusq0  14991  clim  15020  rlim  15021  rlim2  15022  clim2  15030  clim2c  15031  clim0c  15033  rlim0  15034  rlim0lt  15035  ello12r  15043  ello1d  15049  elo12r  15054  rlimresb  15091  rlimcld2  15104  climabs0  15111  rlimo1  15143  lo1add  15153  lo1mul  15154  isercoll  15196  incexclem  15363  sqrt2irr  15773  gcdcllem1  16021  gcdcllem2  16022  dfgcd2  16069  fissn0dvds  16139  dvdslcmf  16151  lcmfledvds  16152  lcmf  16153  lcmfunsnlem1  16157  lcmfunsnlem2lem1  16158  lcmfunsnlem  16161  lcmfdvds  16162  reumodprminv  16320  pc2dvds  16395  pcz  16397  prmpwdvds  16420  infpn2  16429  prmreclem2  16433  prmreclem3  16434  prmreclem5  16436  prmreclem6  16437  vdwlem6  16502  vdwlem8  16504  vdwlem13  16509  vdwnnlem1  16511  vdwnn  16514  ramcl  16545  cshwrepswhash1  16619  prdsleval  16936  imasval  16970  imasaddfnlem  16987  imasvscafn  16996  mrisval  17087  isacs  17108  isacs2  17110  isacs1i  17114  mreacs  17115  acsfn  17116  acsfn2  17120  iscatd  17130  catidex  17131  catideu  17132  cidval  17134  catidd  17137  comfeq  17163  catpropd  17166  ismon  17192  isfunc  17324  isnat  17408  isinito  17456  istermo  17457  isprs  17758  drsdirfi  17766  ispos  17775  lubfval  17810  lubeldm  17813  lubval  17816  lubprop  17818  lublecllem  17820  glbfval  17823  glbeldm  17826  glbval  17829  glbprop  17831  joinval2lem  17840  joinlem  17843  meetval2lem  17854  meetlem  17857  poslubmo  17871  posglbmo  17872  poslubd  17873  isglbd  17969  lubl  17972  lubun  17975  clatleglb  17978  isdlat  17982  ipodrsima  18001  mgm1  18084  gsumval2  18112  sgrp1  18126  mhmima  18205  mndind  18208  gsumwspan  18227  efmndmnd  18270  smndex1mnd  18291  sgrp2rid2  18307  sgrp2rid2ex  18308  sgrp2nmndlem4  18309  pwmnd  18318  dfgrp2  18346  isgrpinv  18374  grpidinv  18377  dfgrp3lem  18415  issubg4  18516  0subg  18522  isnsg2  18526  nsgacs  18532  elnmz  18533  cycsubgcl  18567  ghmrn  18589  ghmnsgima  18600  isga  18639  orbsta  18661  cntzfval  18668  elcntz  18670  resscntz  18680  oppgsubg  18709  symgextfo  18768  gsmsymgreqlem2  18777  gsmsymgreq  18778  pmtrdifel  18826  pmtrdifwrdellem3  18829  pmtrdifwrdel2  18832  psgnunilem2  18841  psgnunilem3  18842  odeq  18896  gexid  18924  gexlem2  18925  gexdvds  18927  isslw  18951  sylow2alem1  18960  sylow2alem2  18961  efgval  19061  efgrelexlemb  19094  efgcpbllemb  19099  abl1  19205  dmdprd  19339  dprd2da  19383  pgpfac1lem5  19420  ring1  19574  isabv  19809  islss  19925  lssacs  19958  reslmhm  20043  islbs  20067  pj1lmhm  20091  lbsacsbs  20147  isrrg  20280  zringlpir  20408  psgndiflemA  20517  ocvfval  20582  elocv  20584  iunocv  20597  frlmlbs  20713  islindf  20728  islinds2  20729  islindf2  20730  lindfrn  20737  lsslindf  20746  islindf4  20754  opsrval  20957  ply1coe  21171  cply1coe0bi  21175  mat0dimcrng  21321  mdetunilem1  21463  mdetunilem9  21471  cpmat  21560  cpmatel  21562  1elcpmat  21566  m2cpminvid2lem  21605  basgen2  21840  bastop1  21844  isclo  21938  ordtbaslem  22039  iscn  22086  cnpval  22087  iscnp  22088  iscnp3  22095  lmbr  22109  lmbr2  22110  lmbrf  22111  cnprest  22140  cnprest2  22141  t0sep  22175  isreg  22183  t1sep2  22220  tgcmp  22252  1stcclb  22295  1stcfb  22296  2ndc1stc  22302  1stcrest  22304  2ndcdisj  22307  islly  22319  isnlly  22320  lly1stc  22347  isref  22360  islocfin  22368  elkgen  22387  kgencn  22407  elpt  22423  elptr  22424  ptcnplem  22472  tx1stc  22501  cnmpt21  22522  kqt0lem  22587  isr0  22588  regr1lem2  22591  r0sep  22599  nrmr0reg  22600  flffbas  22846  cnflf  22853  cnflf2  22854  lmflf  22856  txflf  22857  fclsopni  22866  fclsnei  22870  fclsrest  22875  fcfnei  22886  cnfcf  22893  alexsubb  22897  alexsubALTlem3  22900  qustgplem  22972  tsmsfbas  22979  tsmsres  22995  tsmsf1o  22996  tsmsxplem1  23004  ustval  23054  isust  23055  ustincl  23059  ustdiag  23060  ustinvel  23061  ustexhalf  23062  ust0  23071  utopval  23084  ucnval  23128  isucn  23129  isucn2  23130  ucnima  23132  iscfilu  23139  ispsmet  23156  ismet  23175  isxmet  23176  imasdsf1olem  23225  imasf1oxmet  23227  imasf1omet  23228  metss  23360  met1stc  23373  prdsxmslem2  23381  txmetcnp  23399  metucn  23423  tngngp3  23508  nlmvscn  23539  nmoval  23567  nmolb  23569  qtopbaslem  23610  cncfval  23739  elcncf2  23741  mulc1cncf  23756  cncfmet  23760  evth  23810  lebnumlem3  23814  lebnum  23815  xlebnum  23816  ishtpy  23823  isphtpy  23832  pi1xfr  23906  pi1coghm  23912  isclmp  23948  ipcn  24097  lmmbr2  24110  lmmbr3  24111  lmmbrf  24113  cfilfval  24115  iscfil  24116  fmcfil  24123  caufval  24126  iscau  24127  iscau2  24128  iscau3  24129  iscau4  24130  iscauf  24131  caucfil  24134  cfilresi  24146  causs  24149  lmclim  24154  cmetcusp1  24204  minveclem4c  24276  minveclem2  24277  minveclem3b  24279  minveclem4  24283  minveclem6  24285  minveclem7  24286  ovolicc2lem3  24370  ismbl  24377  dyadmax  24449  dyadmbllem  24450  dyadmbl  24451  opnmbllem  24452  ismbf1  24475  ismbf  24479  mbfeqalem2  24493  mbflimsup  24517  mbfi1fseqlem6  24572  mbfi1flimlem  24574  itg2seq  24594  itg2monolem1  24602  isibl  24617  ply1divex  24988  fta1g  25019  dgrco  25123  plydivex  25144  fta1  25155  vieta1  25159  aannenlem1  25175  aannenlem2  25176  aalioulem2  25180  aalioulem3  25181  ulmval  25226  ulm2  25231  ulmi  25232  ulmres  25234  ulmshftlem  25235  ulmcaulem  25240  ulmcau  25241  ulmss  25243  ulmbdd  25244  ulmdvlem1  25246  ulmdvlem3  25248  pilem2  25298  pilem3  25299  cxpcn3  25588  dmarea  25794  rlimcnp  25802  scvxcvx  25822  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem5  25869  lgambdd  25873  lgamcvglem  25876  isppw2  25951  perfectlem2  26065  2sqlem6  26258  2sqlem10  26263  addsq2reu  26275  2sqreulem1  26281  2sqreunnlem1  26284  dchrisumlema  26323  dchrisumlem2  26325  dchrisumlem3  26326  pntpbnd  26423  pntibndlem3  26427  pntibnd  26428  pntleme  26443  pntlem3  26444  pntlemp  26445  pnt3  26447  istrkgld  26504  axtg5seg  26510  tgcgr4  26576  perpln1  26755  perpln2  26756  isperp  26757  brbtwn2  26950  colinearalg  26955  axsegconlem1  26962  axsegcon  26972  ax5seglem4  26977  ax5seglem5  26978  axlowdim  27006  axeuclidlem  27007  axcontlem1  27009  axcontlem2  27010  axcontlem4  27012  axcontlem5  27013  axcontlem8  27016  axcontlem12  27020  elntg2  27030  uvtxusgr  27444  rgrx0ndm  27635  ewlksfval  27643  wksfval  27651  wwlks  27873  wlkiswwlks2  27913  clwwlk  28020  1conngr  28231  frgrwopregasn  28353  frgrwopregbsn  28354  frgrwopreglem5ALT  28359  frgrregord013  28432  isgrpo  28532  isgrpoi  28533  grpoideu  28544  grpoidinv2  28550  vciOLD  28596  isvclem  28612  cnidOLD  28617  isnvlem  28645  nvi  28649  lnoval  28787  islno  28788  isblo3i  28836  blo3i  28837  blocnilem  28839  ajfval  28844  ubthlem1  28905  ubthlem2  28906  ubthlem3  28907  ubth  28908  minvecolem2  28910  minvecolem3  28911  minvecolem4c  28914  minvecolem4  28915  minvecolem5  28916  minvecolem6  28917  minvecolem7  28918  h2hcau  29014  h2hlm  29015  hilid  29196  hcau  29219  hlimi  29223  hlim2  29227  ocel  29316  adjsym  29868  ellnop  29893  ellnfn  29918  hhcno  29939  hhcnf  29940  lnopeq  30044  elunop2  30048  lnophm  30054  lnconi  30068  lnopcnbd  30071  lnfncnbd  30092  imaelshi  30093  riesz3i  30097  riesz4i  30098  riesz4  30099  riesz1  30100  cnlnadjlem2  30103  cnlnadjlem5  30106  cnlnadjlem8  30109  cnlnadji  30111  nmopadjlei  30123  cnvbraval  30145  leopg  30157  leoppos  30161  mdbr  30329  dmdbr  30334  cdj3i  30476  disjunsn  30606  funcnv5mpt  30679  fgreu  30683  fcnvgreu  30684  xrge0infss  30757  wrdt2ind  30899  resspos  30917  mgccole1  30941  mgccole2  30942  mgcmnt1  30943  mgcmnt2  30944  gsumhashmul  30989  isomnd  31000  inftmrel  31107  isinftm  31108  archiabl  31125  isarchiofld  31189  0nellinds  31234  lindssn  31241  elrspunidl  31274  prmidl  31283  ismxidl  31302  crefeq  31463  zarcmplem  31499  esum2d  31727  sigaval  31745  issgon  31757  isrnmeas  31834  ismbfm  31885  isanmbfm  31889  mbfmcst  31892  elcarsg  31938  sitgval  31965  eulerpartlemd  31999  ballotleme  32129  tgoldbachgt  32309  bnj1185  32440  bnj1385  32479  bnj66  32507  bnj106  32515  bnj155  32526  bnj852  32568  bnj893  32575  bnj1228  32658  bnj1234  32660  bnj1463  32702  nummin  32730  derangenlem  32800  subfacp1lem3  32811  subfacp1lem5  32813  subfacp1lem6  32814  subfacp1  32815  erdszelem8  32827  kur14  32845  cnpconn  32859  resconn  32875  cvmscbv  32887  iscvm  32888  cvmsi  32894  cvmsval  32895  cvmlift3lem2  32949  snmlval  32960  satfv1  32992  fmlasucdisj  33028  satffunlem1lem1  33031  satffunlem2lem1  33033  satfv1fvfmla1  33052  mclsssvlem  33191  mclsval  33192  mclsax  33198  mclsind  33199  dfpo2  33392  dfon2lem9  33437  dfrdg2  33441  dfrdg3  33442  frxp2  33471  xpord2ind  33474  frxp3  33477  xpord3ind  33480  poseq  33482  soseq  33483  naddcllem  33517  naddov2  33520  sltval  33536  nosupprefixmo  33589  noinfprefixmo  33590  nosupcbv  33591  nosupno  33592  nosupdm  33593  nosupfv  33595  nosupres  33596  nosupbnd1lem1  33597  nosupbnd1lem3  33599  nosupbnd1lem5  33601  noinfcbv  33606  noinfno  33607  noinfdm  33608  noinffv  33610  noinfres  33611  noinfbnd1lem3  33614  noinfbnd1lem5  33616  noetalem1  33630  noetalem2  33631  nocvxminlem  33658  brsslt  33666  conway  33679  etasslt  33693  slerec  33699  madebdaylemlrcut  33765  madebday  33766  cofcutr  33778  lrrecfr  33786  fwddifnval  34151  nn0prpwlem  34197  isfne  34214  isfne4  34215  isfne2  34217  isfne3  34218  neibastop3  34237  topmeet  34239  topjoin  34240  filnetlem4  34256  unblimceq0lem  34372  unblimceq0  34373  unbdqndv2  34377  taupilemrplb  35174  csbwrecsg  35184  fin2so  35450  lindsadd  35456  matunitlindflem2  35460  ptrecube  35463  poimirlem2  35465  poimirlem3  35466  poimirlem4  35467  poimirlem24  35487  poimirlem25  35488  poimirlem26  35489  poimirlem27  35490  poimirlem28  35491  poimirlem29  35492  poimirlem30  35493  poimirlem32  35495  poimir  35496  heicant  35498  mblfinlem1  35500  mblfinlem2  35501  voliunnfl  35507  volsupnfl  35508  mbfresfi  35509  itg2addnc  35517  upixp  35573  indexdom  35578  filbcmb  35584  sdclem2  35586  fdc  35589  lmclim2  35602  caures  35604  istotbnd  35613  istotbnd3  35615  sstotbnd  35619  isbnd  35624  heibor  35665  bfp  35668  rrncmslem  35676  isgrpda  35799  idlval  35857  isidl  35858  0idl  35869  unichnidl  35875  pridl  35881  ismaxidl  35884  smprngopr  35896  igenval2  35910  prnc  35911  ispridlc  35914  scottexf  36012  scott0f  36013  riotasvd  36656  islfl  36760  eqlkr  36799  eqlkr3  36801  glbconN  37077  hlsuprexch  37081  ispsubsp  37445  ldilset  37809  isldil  37810  dilsetN  37853  isdilN  37854  trlset  37861  trlval  37862  cdleme27b  38068  cdleme29b  38075  cdleme31so  38079  cdleme31sn1  38081  cdleme31sn1c  38088  cdleme31fv  38090  cdleme40v  38169  istendo  38460  cdlemkid3N  38633  cdlemkid4  38634  cdlemkid5  38635  dihfval  38931  dihval  38932  islpolN  39183  hdmapffval  39526  hdmapfval  39527  hdmapval  39528  hdmapval2lem  39531  hgmapffval  39585  hgmapfval  39586  hgmapval  39587  hgmapvs  39591  sticksstones2  39772  qsalrel  39869  fsuppind  39930  sn-sup2  40088  isnacs  40170  isnacs2  40172  nacsfix  40178  mzpclval  40191  elmzpcl  40192  rencldnfilem  40286  infmrgelbi  40344  pellfundre  40347  pellfundlb  40350  wepwsolem  40511  fnwe2lem2  40520  aomclem8  40530  dfac11  40531  gicabl  40568  islnr3  40584  hbtlem2  40593  hbtlem5  40597  fiinfi  40797  clsk1independent  41274  ntrclsk13  41299  gneispacess2  41374  imo72b2lem0  41394  imo72b2lem2  41396  imo72b2lem1  41398  imo72b2  41402  scottelrankd  41479  mnuop23d  41498  ismnushort  41533  evth2f  42172  evthf  42184  fnchoice  42186  uzwo4  42215  wessf1ornlem  42336  disjinfi  42345  rnmptlb  42401  rnmptbdd  42403  rnmptbd2  42408  rnmptbd  42415  dstregt0  42433  upbdrech2  42461  rexabslelem  42572  rexabsle  42573  uzub  42585  infrpgernmpt  42621  mccl  42757  ellimcabssub0  42776  climf  42781  clim2f  42795  limsupre  42800  clim2cf  42809  clim0cf  42813  climf2  42825  clim2f2  42829  clim2d  42832  limsupref  42844  limsupbnd1f  42845  climinf2  42866  limsuppnf  42870  climinfmpt  42874  climinf3  42875  limsupubuzmpt  42878  limsupmnf  42880  limsupre2lem  42883  limsupre2  42884  limsupmnfuzlem  42885  limsupmnfuz  42886  limsupre2mpt  42889  limsupre3lem  42891  limsupre3  42892  limsupre3mpt  42893  limsupre3uz  42895  limsupreuz  42896  limsupreuzmpt  42898  climuz  42903  liminfreuzlem  42961  liminfreuz  42962  cnrefiisplem  42988  xlimmnfvlem1  42991  xlimmnfv  42993  xlimpnfvlem1  42995  xlimpnfv  42997  xlimmnfmpt  43002  xlimpnfmpt  43003  cncfshift  43033  cncfperiod  43038  fperdvper  43078  dvbdfbdioo  43089  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnprodlem3  43107  stoweidlem5  43164  stoweidlem9  43168  stoweidlem15  43174  stoweidlem16  43175  stoweidlem27  43186  stoweidlem28  43187  stoweidlem31  43190  stoweidlem34  43193  stoweidlem37  43196  stoweidlem46  43205  stoweidlem48  43207  stoweidlem51  43210  stoweidlem52  43211  stoweidlem59  43218  wallispilem3  43226  stirlinglem13  43245  fourierdlem2  43268  fourierdlem3  43269  fourierdlem16  43282  fourierdlem20  43286  fourierdlem21  43287  fourierdlem22  43288  fourierdlem25  43291  fourierdlem39  43305  fourierdlem42  43308  fourierdlem54  43319  fourierdlem64  43329  fourierdlem77  43342  fourierdlem83  43348  fourierdlem103  43368  fourierdlem104  43369  subsaliuncllem  43514  iundjiun  43616  meaiunincf  43639  caragenval  43649  isome  43650  caragenel  43651  omessle  43654  ovnlerp  43718  hoidmvlelem3  43753  hoidmvle  43756  issmflem  43878  issmfgt  43907  smfmullem2  43941  smfmullem4  43943  smfmul  43944  smfsuplem2  43960  smfsup  43962  smfinflem  43965  smfinf  43966  cfsetsnfsetf  44167  cbvral2  44210  2reu8i  44220  2reuimp0  44221  dfdfat2  44235  iccpart  44484  iccpartigtl  44491  paireqne  44579  reupr  44590  perfectALTVlem2  44790  bgoldbachlt  44881  tgoldbachlt  44884  isomgreqve  44893  isomushgr  44894  isomuspgrlem2  44901  isomgrsym  44904  isomgrtr  44907  ushrisomgr  44909  upwlksfval  44913  mgmhmima  44972  nn0mnd  44989  lidlmsgrp  45100  lidlrng  45101  uzlidlring  45103  ply1mulgsumlem1  45343  ply1mulgsumlem2  45344  linindslinci  45405  lindslinindsimp1  45414  lindslinindsimp2lem5  45419  lindslinindsimp2  45420  linds0  45422  lindsrng01  45425  snlindsntor  45428  lmod1  45449  ldepsnlinc  45465  bigoval  45511  elbigo2r  45515  nn0sumshdiglem2  45584  eenglngeehlnmlem1  45699  eenglngeehlnmlem2  45700  lubeldm2d  45868  glbeldm2d  45869  lubsscl  45870  glbsscl  45871  ipolubdm  45889  ipolub  45890  ipoglbdm  45892  ipoglb  45893  isthincd2lem2  45933  setrec1lem2  46008