Theorem ralbidv 3113

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

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

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 397  df-ral 3070

This theorem is referenced by:  2ralbidv  3130  rexralbidv  3231  cbvral2vw  3397  cbvral2v  3400  rspceaimv  3566  rspc2  3569  rspc2v  3571  rspc3v  3574  reu6i  3664  reu7  3668  sbcralt  3806  reu8nf  3811  raaan  4452  raaanv  4453  raaan2  4456  2reu4lem  4457  reusngf  4609  2ralsng  4613  rexreusng  4616  reuprg0  4639  issn  4764  2ralunsn  4827  elintg  4888  elintrabg  4893  eliin  4930  disjprgw  5070  disjprg  5071  disjxun  5073  brralrspcev  5135  reusv2lem2  5323  reusv3  5329  poeq1  5507  solin  5529  somo  5541  frirr  5567  fr2nr  5568  frminex  5570  wereu2  5587  posn  5673  frsn  5675  ralxpf  5758  cnvpo  6194  reu3op  6199  reuop  6200  dfpo2  6203  frpomin  6247  fnmptfvd  6927  iinpreima  6955  dff4  6986  dff13f  7138  fpropnf1  7149  eusvobj2  7277  ovanraleqv  7308  f1opr  7340  ofreq  7546  sorpssuni  7594  sorpssint  7595  fr3nr  7631  onssmin  7651  funcnvuni  7787  f1oweALT  7824  frxp  7976  frecseq123  8107  csbfrecsg  8109  frrlem1  8111  frrlem13  8123  wrecseq123OLD  8140  wfrlem1OLD  8148  wfrlem3OLDa  8151  wfrlem15OLD  8163  smoeq  8190  tfrlem12  8229  tz7.48lem  8281  elixp2  8698  undifixp  8731  xpf1o  8935  nneneq  9001  nneneqOLD  9013  ac6sfi  9067  frfi  9068  fipreima  9134  indexfi  9136  marypha1lem  9201  marypha1  9202  supeq1  9213  supeq3  9217  supmo  9220  eqsup  9224  supub  9227  suplub  9228  sup0  9234  supisoex  9242  eqinf  9252  infval  9254  infmo  9263  oieq1  9280  ordtypecbv  9285  ordtypelem3  9288  ordtypelem6  9291  ordtypelem7  9292  ordtypelem9  9294  wemaplem1  9314  wemaplem2  9315  zfregcl  9362  oemapval  9450  oemapvali  9451  cantnf  9460  wemapwe  9464  ttrcleq  9476  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  rankval3b  9593  unbndrank  9609  rankunb  9617  rankuni2b  9620  tcrank  9651  scottex  9652  scottexs  9654  scott0s  9655  bnd2  9660  updjud  9701  dfac8clem  9797  ac5num  9801  acni  9810  acni2  9811  alephval3  9875  dfac4  9887  dfac5lem5  9892  dfac5  9893  dfac2a  9894  dfac2b  9895  dfacacn  9906  kmlem2  9916  kmlem13  9927  cflem  10011  cflecard  10018  cfeq0  10021  cfsuc  10022  cfflb  10024  cofsmo  10034  cfsmolem  10035  cfcoflem  10037  coftr  10038  alephsing  10041  fin23lem11  10082  isfin3ds  10094  fin23lem17  10103  fin23lem39  10115  isf33lem  10131  isf34lem6  10145  fin1a2lem13  10177  hsmexlem4  10194  hsmex  10197  axcc2lem  10201  axcc3  10203  dcomex  10212  axdc2lem  10213  axdc3lem2  10216  axdc3lem3  10217  axdc3  10219  axdc4lem  10220  axcclem  10222  zorn2lem2  10262  zorn2lem7  10267  zorn2g  10268  zornn0g  10270  ttukeylem7  10280  axdclem2  10285  brdom3  10293  brdom7disj  10296  brdom6disj  10297  alephval2  10337  inar1  10540  axgroth6  10593  pinq  10692  nqereu  10694  prlem934  10798  supexpr  10819  supsrlem  10876  axpre-sup  10934  dedekind  11147  dedekindle  11148  fiminre2  11932  lbreu  11934  sup2  11940  infm3  11943  nnsub  12026  uzwo  12660  nnwof  12663  ublbneg  12682  lbzbi  12685  zsupss  12686  uzsupss  12689  uzwo3  12692  zmax  12694  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem4  12729  rpnnen1lem5  12730  xrsupsslem  13050  xrinfmsslem  13051  xrsupss  13052  xrinfmss  13053  flval2  13543  axdc4uzlem  13712  ssnn0fi  13714  fsuppmapnn0fiubex  13721  faclbnd4lem4  14019  bccl  14045  hashgt12el  14146  hashbc  14174  hashge2el2dif  14203  wrdind  14444  wrd2ind  14445  rexanre  15067  rexico  15074  cau4  15077  reusq0  15183  clim  15212  rlim  15213  rlim2  15214  clim2  15222  clim2c  15223  clim0c  15225  rlim0  15226  rlim0lt  15227  ello12r  15235  ello1d  15241  elo12r  15246  rlimresb  15283  rlimcld2  15296  climabs0  15303  rlimo1  15335  lo1add  15345  lo1mul  15346  isercoll  15388  incexclem  15557  sqrt2irr  15967  gcdcllem1  16215  gcdcllem2  16216  dfgcd2  16263  fissn0dvds  16333  dvdslcmf  16345  lcmfledvds  16346  lcmf  16347  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem  16355  lcmfdvds  16356  reumodprminv  16514  pc2dvds  16589  pcz  16591  prmpwdvds  16614  infpn2  16623  prmreclem2  16627  prmreclem3  16628  prmreclem5  16630  prmreclem6  16631  vdwlem6  16696  vdwlem8  16698  vdwlem13  16703  vdwnnlem1  16705  vdwnn  16708  ramcl  16739  cshwrepswhash1  16813  prdsleval  17197  imasval  17231  imasaddfnlem  17248  imasvscafn  17257  mrisval  17348  isacs  17369  isacs2  17371  isacs1i  17375  mreacs  17376  acsfn  17377  acsfn2  17381  iscatd  17391  catidex  17392  catideu  17393  cidval  17395  catidd  17398  comfeq  17424  catpropd  17427  ismon  17454  isfunc  17588  isnat  17672  isinito  17720  istermo  17721  isprs  18024  drsdirfi  18032  ispos  18041  lubfval  18077  lubeldm  18080  lubval  18083  lubprop  18085  lublecllem  18087  glbfval  18090  glbeldm  18093  glbval  18096  glbprop  18098  joinval2lem  18107  joinlem  18110  meetval2lem  18121  meetlem  18124  poslubmo  18138  posglbmo  18139  poslubd  18140  isglbd  18236  lubl  18239  lubun  18242  clatleglb  18245  isdlat  18249  ipodrsima  18268  mgm1  18351  gsumval2  18379  sgrp1  18393  mhmima  18472  mndind  18475  gsumwspan  18494  efmndmnd  18537  smndex1mnd  18558  sgrp2rid2  18574  sgrp2rid2ex  18575  sgrp2nmndlem4  18576  pwmnd  18585  dfgrp2  18613  isgrpinv  18641  grpidinv  18644  dfgrp3lem  18682  issubg4  18783  0subg  18789  isnsg2  18793  nsgacs  18799  elnmz  18800  cycsubgcl  18834  ghmrn  18856  ghmnsgima  18867  isga  18906  orbsta  18928  cntzfval  18935  elcntz  18937  resscntz  18947  oppgsubg  18979  symgextfo  19039  gsmsymgreqlem2  19048  gsmsymgreq  19049  pmtrdifel  19097  pmtrdifwrdellem3  19100  pmtrdifwrdel2  19103  psgnunilem2  19112  psgnunilem3  19113  odeq  19167  gexid  19195  gexlem2  19196  gexdvds  19198  isslw  19222  sylow2alem1  19231  sylow2alem2  19232  efgval  19332  efgrelexlemb  19365  efgcpbllemb  19370  abl1  19476  dmdprd  19610  dprd2da  19654  pgpfac1lem5  19691  ring1  19850  isabv  20088  islss  20205  lssacs  20238  reslmhm  20323  islbs  20347  pj1lmhm  20371  lbsacsbs  20427  isrrg  20568  zringlpir  20698  psgndiflemA  20815  ocvfval  20880  elocv  20882  iunocv  20895  frlmlbs  21013  islindf  21028  islinds2  21029  islindf2  21030  lindfrn  21037  lsslindf  21046  islindf4  21054  opsrval  21256  ply1coe  21476  cply1coe0bi  21480  mat0dimcrng  21628  mdetunilem1  21770  mdetunilem9  21778  cpmat  21867  cpmatel  21869  1elcpmat  21873  m2cpminvid2lem  21912  basgen2  22148  bastop1  22152  isclo  22247  ordtbaslem  22348  iscn  22395  cnpval  22396  iscnp  22397  iscnp3  22404  lmbr  22418  lmbr2  22419  lmbrf  22420  cnprest  22449  cnprest2  22450  t0sep  22484  isreg  22492  t1sep2  22529  tgcmp  22561  1stcclb  22604  1stcfb  22605  2ndc1stc  22611  1stcrest  22613  2ndcdisj  22616  islly  22628  isnlly  22629  lly1stc  22656  isref  22669  islocfin  22677  elkgen  22696  kgencn  22716  elpt  22732  elptr  22733  ptcnplem  22781  tx1stc  22810  cnmpt21  22831  kqt0lem  22896  isr0  22897  regr1lem2  22900  r0sep  22908  nrmr0reg  22909  flffbas  23155  cnflf  23162  cnflf2  23163  lmflf  23165  txflf  23166  fclsopni  23175  fclsnei  23179  fclsrest  23184  fcfnei  23195  cnfcf  23202  alexsubb  23206  alexsubALTlem3  23209  qustgplem  23281  tsmsfbas  23288  tsmsres  23304  tsmsf1o  23305  tsmsxplem1  23313  ustval  23363  isust  23364  ustincl  23368  ustdiag  23369  ustinvel  23370  ustexhalf  23371  ust0  23380  utopval  23393  ucnval  23438  isucn  23439  isucn2  23440  ucnima  23442  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  imasdsf1olem  23535  imasf1oxmet  23537  imasf1omet  23538  metss  23673  met1stc  23686  prdsxmslem2  23694  txmetcnp  23712  metucn  23736  tngngp3  23829  nlmvscn  23860  nmoval  23888  nmolb  23890  qtopbaslem  23931  cncfval  24060  elcncf2  24062  mulc1cncf  24077  cncfmet  24081  evth  24131  lebnumlem3  24135  lebnum  24136  xlebnum  24137  ishtpy  24144  isphtpy  24153  pi1xfr  24227  pi1coghm  24233  isclmp  24269  ipcn  24419  lmmbr2  24432  lmmbr3  24433  lmmbrf  24435  cfilfval  24437  iscfil  24438  fmcfil  24445  caufval  24448  iscau  24449  iscau2  24450  iscau3  24451  iscau4  24452  iscauf  24453  caucfil  24456  cfilresi  24468  causs  24471  lmclim  24476  cmetcusp1  24526  minveclem4c  24598  minveclem2  24599  minveclem3b  24601  minveclem4  24605  minveclem6  24607  minveclem7  24608  ovolicc2lem3  24692  ismbl  24699  dyadmax  24771  dyadmbllem  24772  dyadmbl  24773  opnmbllem  24774  ismbf1  24797  ismbf  24801  mbfeqalem2  24815  mbflimsup  24839  mbfi1fseqlem6  24894  mbfi1flimlem  24896  itg2seq  24916  itg2monolem1  24924  isibl  24939  ply1divex  25310  fta1g  25341  dgrco  25445  plydivex  25466  fta1  25477  vieta1  25481  aannenlem1  25497  aannenlem2  25498  aalioulem2  25502  aalioulem3  25503  ulmval  25548  ulm2  25553  ulmi  25554  ulmres  25556  ulmshftlem  25557  ulmcaulem  25562  ulmcau  25563  ulmss  25565  ulmbdd  25566  ulmdvlem1  25568  ulmdvlem3  25570  pilem2  25620  pilem3  25621  cxpcn3  25910  dmarea  26116  rlimcnp  26124  scvxcvx  26144  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgambdd  26195  lgamcvglem  26198  isppw2  26273  perfectlem2  26387  2sqlem6  26580  2sqlem10  26585  addsq2reu  26597  2sqreulem1  26603  2sqreunnlem1  26606  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  pntpbnd  26745  pntibndlem3  26749  pntibnd  26750  pntleme  26765  pntlem3  26766  pntlemp  26767  pnt3  26769  istrkgld  26829  axtg5seg  26835  tgcgr4  26901  perpln1  27080  perpln2  27081  isperp  27082  brbtwn2  27282  colinearalg  27287  axsegconlem1  27294  axsegcon  27304  ax5seglem4  27309  ax5seglem5  27310  axlowdim  27338  axeuclidlem  27339  axcontlem1  27341  axcontlem2  27342  axcontlem4  27344  axcontlem5  27345  axcontlem8  27348  axcontlem12  27352  elntg2  27362  uvtxusgr  27778  rgrx0ndm  27969  ewlksfval  27977  wksfval  27985  wwlks  28209  wlkiswwlks2  28249  clwwlk  28356  1conngr  28567  frgrwopregasn  28689  frgrwopregbsn  28690  frgrwopreglem5ALT  28695  frgrregord013  28768  isgrpo  28868  isgrpoi  28869  grpoideu  28880  grpoidinv2  28886  vciOLD  28932  isvclem  28948  cnidOLD  28953  isnvlem  28981  nvi  28985  lnoval  29123  islno  29124  isblo3i  29172  blo3i  29173  blocnilem  29175  ajfval  29180  ubthlem1  29241  ubthlem2  29242  ubthlem3  29243  ubth  29244  minvecolem2  29246  minvecolem3  29247  minvecolem4c  29250  minvecolem4  29251  minvecolem5  29252  minvecolem6  29253  minvecolem7  29254  h2hcau  29350  h2hlm  29351  hilid  29532  hcau  29555  hlimi  29559  hlim2  29563  ocel  29652  adjsym  30204  ellnop  30229  ellnfn  30254  hhcno  30275  hhcnf  30276  lnopeq  30380  elunop2  30384  lnophm  30390  lnconi  30404  lnopcnbd  30407  lnfncnbd  30428  imaelshi  30429  riesz3i  30433  riesz4i  30434  riesz4  30435  riesz1  30436  cnlnadjlem2  30439  cnlnadjlem5  30442  cnlnadjlem8  30445  cnlnadji  30447  nmopadjlei  30459  cnvbraval  30481  leopg  30493  leoppos  30497  mdbr  30665  dmdbr  30670  cdj3i  30812  disjunsn  30942  funcnv5mpt  31014  fgreu  31018  fcnvgreu  31019  xrge0infss  31092  wrdt2ind  31234  resspos  31253  mgccole1  31277  mgccole2  31278  mgcmnt1  31279  mgcmnt2  31280  gsumhashmul  31325  isomnd  31336  inftmrel  31443  isinftm  31444  archiabl  31461  isarchiofld  31525  0nellinds  31575  lindssn  31582  elrspunidl  31615  prmidl  31624  ismxidl  31643  crefeq  31804  zarcmplem  31840  esum2d  32070  sigaval  32088  issgon  32100  isrnmeas  32177  ismbfm  32228  isanmbfm  32232  mbfmcst  32235  elcarsg  32281  sitgval  32308  eulerpartlemd  32342  ballotleme  32472  tgoldbachgt  32652  bnj1185  32782  bnj1385  32821  bnj66  32849  bnj106  32857  bnj155  32868  bnj852  32910  bnj893  32917  bnj1228  33000  bnj1234  33002  bnj1463  33044  nummin  33072  derangenlem  33142  subfacp1lem3  33153  subfacp1lem5  33155  subfacp1lem6  33156  subfacp1  33157  erdszelem8  33169  kur14  33187  cnpconn  33201  resconn  33217  cvmscbv  33229  iscvm  33230  cvmsi  33236  cvmsval  33237  cvmlift3lem2  33291  snmlval  33302  satfv1  33334  fmlasucdisj  33370  satffunlem1lem1  33373  satffunlem2lem1  33375  satfv1fvfmla1  33394  mclsssvlem  33533  mclsval  33534  mclsax  33540  mclsind  33541  dfon2lem9  33776  dfrdg2  33780  dfrdg3  33781  frxp2  33800  xpord2ind  33803  frxp3  33806  xpord3ind  33809  poseq  33811  soseq  33812  naddcllem  33840  naddov2  33843  sltval  33859  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupno  33915  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem5  33924  noinfcbv  33929  noinfno  33930  noinfdm  33931  noinffv  33933  noinfres  33934  noinfbnd1lem3  33937  noinfbnd1lem5  33939  noetalem1  33953  noetalem2  33954  nocvxminlem  33981  brsslt  33989  conway  34002  etasslt  34016  slerec  34022  madebdaylemlrcut  34088  madebday  34089  cofcutr  34101  lrrecfr  34109  fwddifnval  34474  nn0prpwlem  34520  isfne  34537  isfne4  34538  isfne2  34540  isfne3  34541  neibastop3  34560  topmeet  34562  topjoin  34563  filnetlem4  34579  unblimceq0lem  34695  unblimceq0  34696  unbdqndv2  34700  taupilemrplb  35500  fin2so  35773  lindsadd  35779  matunitlindflem2  35783  ptrecube  35786  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimirlem32  35818  poimir  35819  heicant  35821  mblfinlem1  35823  mblfinlem2  35824  voliunnfl  35830  volsupnfl  35831  mbfresfi  35832  itg2addnc  35840  upixp  35896  indexdom  35901  filbcmb  35907  sdclem2  35909  fdc  35912  lmclim2  35925  caures  35927  istotbnd  35936  istotbnd3  35938  sstotbnd  35942  isbnd  35947  heibor  35988  bfp  35991  rrncmslem  35999  isgrpda  36122  idlval  36180  isidl  36181  0idl  36192  unichnidl  36198  pridl  36204  ismaxidl  36207  smprngopr  36219  igenval2  36233  prnc  36234  ispridlc  36237  scottexf  36335  scott0f  36336  riotasvd  36977  islfl  37081  eqlkr  37120  eqlkr3  37122  glbconN  37398  hlsuprexch  37402  ispsubsp  37766  ldilset  38130  isldil  38131  dilsetN  38174  isdilN  38175  trlset  38182  trlval  38183  cdleme27b  38389  cdleme29b  38396  cdleme31so  38400  cdleme31sn1  38402  cdleme31sn1c  38409  cdleme31fv  38411  cdleme40v  38490  istendo  38781  cdlemkid3N  38954  cdlemkid4  38955  cdlemkid5  38956  dihfval  39252  dihval  39253  islpolN  39504  hdmapffval  39847  hdmapfval  39848  hdmapval  39849  hdmapval2lem  39852  hgmapffval  39906  hgmapfval  39907  hgmapval  39908  hgmapvs  39912  sticksstones2  40110  qsalrel  40222  fsuppind  40286  sn-sup2  40446  isnacs  40533  isnacs2  40535  nacsfix  40541  mzpclval  40554  elmzpcl  40555  rencldnfilem  40649  infmrgelbi  40707  pellfundre  40710  pellfundlb  40713  wepwsolem  40874  fnwe2lem2  40883  aomclem8  40893  dfac11  40894  gicabl  40931  islnr3  40947  hbtlem2  40956  hbtlem5  40960  fiinfi  41187  clsk1independent  41663  ntrclsk13  41688  gneispacess2  41763  imo72b2lem0  41783  imo72b2lem2  41785  imo72b2lem1  41787  imo72b2  41790  scottelrankd  41872  mnuop23d  41891  ismnushort  41926  evth2f  42565  evthf  42577  fnchoice  42579  uzwo4  42608  wessf1ornlem  42729  disjinfi  42738  rnmptlb  42795  rnmptbdd  42797  rnmptbd2  42802  rnmptbd  42809  dstregt0  42827  upbdrech2  42854  rexabslelem  42965  rexabsle  42966  uzub  42978  infrpgernmpt  43012  mccl  43146  ellimcabssub0  43165  climf  43170  clim2f  43184  limsupre  43189  clim2cf  43198  clim0cf  43202  climf2  43214  clim2f2  43218  clim2d  43221  limsupref  43233  limsupbnd1f  43234  climinf2  43255  limsuppnf  43259  climinfmpt  43263  climinf3  43264  limsupubuzmpt  43267  limsupmnf  43269  limsupre2lem  43272  limsupre2  43273  limsupmnfuzlem  43274  limsupmnfuz  43275  limsupre2mpt  43278  limsupre3lem  43280  limsupre3  43281  limsupre3mpt  43282  limsupre3uz  43284  limsupreuz  43285  limsupreuzmpt  43287  climuz  43292  liminfreuzlem  43350  liminfreuz  43351  cnrefiisplem  43377  xlimmnfvlem1  43380  xlimmnfv  43382  xlimpnfvlem1  43384  xlimpnfv  43386  xlimmnfmpt  43391  xlimpnfmpt  43392  cncfshift  43422  cncfperiod  43427  fperdvper  43467  dvbdfbdioo  43478  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem3  43496  stoweidlem5  43553  stoweidlem9  43557  stoweidlem15  43563  stoweidlem16  43564  stoweidlem27  43575  stoweidlem28  43576  stoweidlem31  43579  stoweidlem34  43582  stoweidlem37  43585  stoweidlem46  43594  stoweidlem48  43596  stoweidlem51  43599  stoweidlem52  43600  stoweidlem59  43607  wallispilem3  43615  stirlinglem13  43634  fourierdlem2  43657  fourierdlem3  43658  fourierdlem16  43671  fourierdlem20  43675  fourierdlem21  43676  fourierdlem22  43677  fourierdlem25  43680  fourierdlem39  43694  fourierdlem42  43697  fourierdlem54  43708  fourierdlem64  43718  fourierdlem77  43731  fourierdlem83  43737  fourierdlem103  43757  fourierdlem104  43758  subsaliuncllem  43903  iundjiun  44005  meaiunincf  44028  caragenval  44038  isome  44039  caragenel  44040  omessle  44043  ovnlerp  44107  hoidmvlelem3  44142  hoidmvle  44145  issmflem  44272  issmfgt  44301  smfmullem2  44337  smfmullem4  44339  smfmul  44340  smfsuplem2  44356  smfsup  44358  smfinflem  44361  smfinf  44362  cfsetsnfsetf  44563  cbvral2  44606  2reu8i  44616  2reuimp0  44617  dfdfat2  44631  iccpart  44879  iccpartigtl  44886  paireqne  44974  reupr  44985  perfectALTVlem2  45185  bgoldbachlt  45276  tgoldbachlt  45279  isomgreqve  45288  isomushgr  45289  isomuspgrlem2  45296  isomgrsym  45299  isomgrtr  45302  ushrisomgr  45304  upwlksfval  45308  mgmhmima  45367  nn0mnd  45384  lidlmsgrp  45495  lidlrng  45496  uzlidlring  45498  ply1mulgsumlem1  45738  ply1mulgsumlem2  45739  linindslinci  45800  lindslinindsimp1  45809  lindslinindsimp2lem5  45814  lindslinindsimp2  45815  linds0  45817  lindsrng01  45820  snlindsntor  45823  lmod1  45844  ldepsnlinc  45860  bigoval  45906  elbigo2r  45910  nn0sumshdiglem2  45979  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  lubeldm2d  46263  glbeldm2d  46264  lubsscl  46265  glbsscl  46266  ipolubdm  46284  ipolub  46285  ipoglbdm  46287  ipoglb  46288  isthincd2lem2  46328  setrec1lem2  46405