Theorem ralbidv 2969

Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	ralbidva 2968	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901

This theorem is referenced by:  2ralbidv  2972  rexralbidv  3040  raleqbi1dv  3123  raleqbidv  3129  cbvral2v  3155  rspc2  3292  rspc3v  3296  reu6i  3364  reu7  3368  sbcralt  3477  raaan  4032  2ralsng  4167  issn  4303  2ralunsn  4361  elintg  4418  elintgOLD  4419  elintrabg  4424  eliin  4461  disjprg  4578  disjxun  4581  reusv2lem2  4795  reusv2lem2OLD  4796  reusv3  4802  poeq1  4962  somo  4993  frirr  5015  fr2nr  5016  frminex  5018  wereu2  5035  posn  5110  frsn  5112  ralxpf  5190  cnvpo  5590  fnmptfvd  6228  iinpreima  6253  dff4  6281  dff13f  6417  eusvobj2  6542  ofreq  6798  sorpssuni  6844  sorpssint  6845  fr3nr  6871  onssmin  6889  funcnvuni  7012  f1oweALT  7043  frxp  7174  wrecseq123  7295  wfrlem1  7301  wfrlem3a  7304  wfrlem15  7316  smoeq  7334  tfrlem12  7372  tz7.48lem  7423  elixp2  7798  undifixp  7830  xpf1o  8007  nneneq  8028  ac6sfi  8089  frfi  8090  fipreima  8155  indexfi  8157  marypha1lem  8222  marypha1  8223  supeq1  8234  supeq3  8238  supmo  8241  eqsup  8245  supub  8248  suplub  8249  sup0  8255  supisoex  8263  eqinf  8273  infval  8275  infmo  8284  oieq1  8300  ordtypecbv  8305  ordtypelem3  8308  ordtypelem6  8311  ordtypelem7  8312  ordtypelem9  8314  wemaplem1  8334  wemaplem2  8335  zfregcl  8382  zfregclOLD  8384  oemapval  8463  oemapvali  8464  cantnf  8473  wemapwe  8477  rankval3b  8572  unbndrank  8588  rankunb  8596  rankuni2b  8599  tcrank  8630  scottex  8631  scottexs  8633  scott0s  8634  bnd2  8639  dfac8clem  8738  ac5num  8742  acni  8751  acni2  8752  alephval3  8816  dfac4  8828  dfac5lem5  8833  dfac5  8834  dfac2a  8835  dfac2  8836  dfacacn  8846  kmlem2  8856  kmlem13  8867  cflem  8951  cflecard  8958  cfeq0  8961  cfsuc  8962  cfflb  8964  cofsmo  8974  cfsmolem  8975  cfcoflem  8977  coftr  8978  alephsing  8981  fin23lem11  9022  isfin3ds  9034  fin23lem17  9043  fin23lem39  9055  isf33lem  9071  isf34lem6  9085  fin1a2lem13  9117  hsmexlem4  9134  hsmex  9137  axcc2lem  9141  axcc3  9143  dcomex  9152  axdc2lem  9153  axdc3lem2  9156  axdc3lem3  9157  axdc3  9159  axdc4lem  9160  axcclem  9162  zorn2lem2  9202  zorn2lem7  9207  zorn2g  9208  zornn0g  9210  ttukeylem7  9220  axdclem2  9225  brdom3  9231  brdom7disj  9234  brdom6disj  9235  alephval2  9273  inar1  9476  axgroth6  9529  pinq  9628  nqereu  9630  prlem934  9734  supexpr  9755  supsrlem  9811  axpre-sup  9869  dedekind  10079  dedekindle  10080  fimaxre2  10848  fiminre  10851  lbreu  10852  sup2  10858  infm3  10861  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  supmul  10872  nnsub  10936  uzwo  11627  nnwof  11630  ublbneg  11649  lbzbi  11652  zsupss  11653  uzsupss  11656  uzwo3  11659  zmax  11661  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  xrsupsslem  12009  xrinfmsslem  12010  xrsupss  12011  xrinfmss  12012  iccsupr  12137  supicc  12191  supiccub  12192  supicclub  12193  flval2  12477  flval3  12478  fsequb  12636  axdc4uzlem  12644  ssnn0fi  12646  fsuppmapnn0fiubex  12654  faclbnd4lem4  12945  bccl  12971  hashgt12el  13070  hashbc  13094  hashge2el2dif  13117  wrdind  13328  wrd2ind  13329  sqrlem3  13833  rexanre  13934  rexico  13941  cau4  13944  caubnd2  13945  caubnd  13946  clim  14073  rlim  14074  rlim2  14075  rlim2lt  14076  rlim3  14077  clim2  14083  clim2c  14084  clim0c  14086  rlim0  14087  rlim0lt  14088  ello12r  14096  ello1d  14102  lo1bdd2  14103  lo1bddrp  14104  elo12r  14107  rlimconst  14123  rlimresb  14144  rlimcld2  14157  climabs0  14164  rlimcn2  14169  reccn2  14175  cn1lem  14176  rlimo1  14195  o1rlimmul  14197  lo1add  14205  lo1mul  14206  isercoll  14246  caucvgrlem  14251  incexclem  14407  climcnds  14422  divrcnv  14423  ruclem12  14809  sqrt2irr  14817  gcdcllem1  15059  gcdcllem2  15060  dfgcd2  15101  fissn0dvds  15170  dvdslcmf  15182  lcmfledvds  15183  lcmf  15184  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem  15192  lcmfdvds  15193  maxprmfct  15259  reumodprminv  15347  pc2dvds  15421  pcz  15423  prmpwdvds  15446  infpn2  15455  prmreclem1  15458  prmreclem2  15459  prmreclem3  15460  prmreclem5  15462  prmreclem6  15463  vdwlem6  15528  vdwlem8  15530  vdwlem13  15535  vdwnnlem1  15537  vdwnn  15540  ramz  15567  ramcl  15571  cshwrepswhash1  15647  prdsleval  15960  imasval  15994  imasaddfnlem  16011  imasvscafn  16020  mrisval  16113  isacs  16135  isacs2  16137  isacs1i  16141  mreacs  16142  acsfn  16143  acsfn2  16147  iscatd  16157  catidex  16158  catideu  16159  cidval  16161  catidd  16164  comfeq  16189  catpropd  16192  ismon  16216  isfunc  16347  isnat  16430  isinito  16473  istermo  16474  isprs  16753  drsdirfi  16761  ispos  16770  lubfval  16801  lubeldm  16804  lubval  16807  lubprop  16809  lublecllem  16811  glbfval  16814  glbeldm  16817  glbval  16820  glbprop  16822  joinval2lem  16831  joinlem  16834  meetval2lem  16845  meetlem  16848  isglbd  16940  lubl  16943  lubun  16946  clatleglb  16949  poslubmo  16969  posglbmo  16970  poslubd  16971  ipodrsima  16988  isdlat  17016  mgm1  17080  mgmidmo  17082  ismgmid  17087  ismgmid2  17090  mgmidsssn0  17092  gsumvalx  17093  gsumress  17099  gsumval2  17103  sgrp1  17116  ismndd  17136  mnd1  17154  mhmima  17186  mrcmndind  17189  gsumvallem2  17195  gsumwspan  17206  sgrp2rid2  17236  sgrp2rid2ex  17237  sgrp2nmndlem4  17238  dfgrp2  17270  isgrpinv  17295  grpidinv  17298  dfgrp3lem  17336  mhmmnd  17360  issubg4  17436  0subg  17442  cycsubgcl  17443  isnsg2  17447  nsgacs  17453  elnmz  17456  ghmrn  17496  ghmnsgima  17507  isga  17547  orbsta  17569  cntzfval  17576  elcntz  17578  resscntz  17587  oppgsubg  17616  symgextfo  17665  gsmsymgreqlem2  17674  gsmsymgreq  17675  pmtrdifel  17723  pmtrdifwrdellem3  17726  pmtrdifwrdel2  17729  psgnunilem2  17738  psgnunilem3  17739  odeq  17792  gexid  17819  gexlem2  17820  gexdvds  17822  isslw  17846  pgpssslw  17852  sylow2alem1  17855  sylow2alem2  17856  efgval  17953  efgrelexlemb  17986  efgcpbllemb  17991  gexex  18079  abl1  18092  dmdprd  18220  dprd2da  18264  pgpfac1lem5  18301  ring1  18425  isabv  18642  islss  18756  lssacs  18788  reslmhm  18873  islbs  18897  pj1lmhm  18921  lbsacsbs  18977  isrrg  19109  opsrval  19295  ply1coe  19487  cply1coe0bi  19491  zringlpir  19656  psgndiflemA  19766  ocvfval  19829  elocv  19831  iunocv  19844  frlmlbs  19955  islindf  19970  islinds2  19971  islindf2  19972  lindfrn  19979  lsslindf  19988  islindf4  19996  mat0dimcrng  20095  mdetunilem1  20237  mdetunilem9  20245  cpmat  20333  cpmatel  20335  1elcpmat  20339  m2cpminvid2lem  20378  chfacffsupp  20480  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  basgen2  20604  bastop1  20608  isclo  20701  ordtbaslem  20802  iscn  20849  cnpval  20850  iscnp  20851  iscnp3  20858  lmbr  20872  lmbr2  20873  lmbrf  20874  cnprest  20903  cnprest2  20904  t0sep  20938  isreg  20946  t1sep2  20983  tgcmp  21014  1stcclb  21057  1stcfb  21058  2ndc1stc  21064  1stcrest  21066  2ndcdisj  21069  islly  21081  isnlly  21082  lly1stc  21109  isref  21122  islocfin  21130  elkgen  21149  kgencn  21169  elpt  21185  elptr  21186  ptcnplem  21234  tx1stc  21263  cnmpt21  21284  kqt0lem  21349  isr0  21350  regr1lem2  21353  r0sep  21361  nrmr0reg  21362  flffbas  21609  cnflf  21616  cnflf2  21617  lmflf  21619  txflf  21620  fclsopni  21629  fclsnei  21633  fclsrest  21638  fcfnei  21649  cnfcf  21656  alexsubb  21660  alexsubALTlem3  21663  qustgplem  21734  tsmsfbas  21741  tsmsgsum  21752  tsmsres  21757  tsmsf1o  21758  tsmsxplem1  21766  tsmsxp  21768  ustval  21816  isust  21817  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ust0  21833  utopval  21846  ucnval  21891  isucn  21892  isucn2  21893  ucnima  21895  iscfilu  21902  ispsmet  21919  ismet  21938  isxmet  21939  imasdsf1olem  21988  imasf1oxmet  21990  imasf1omet  21991  metss  22123  met1stc  22136  prdsxmslem2  22144  metcnpi3  22161  txmetcnp  22162  metucn  22186  tngngp3  22270  nlmvscn  22301  nrginvrcnlem  22305  nmoval  22329  nmolb  22331  nghmcn  22359  qtopbaslem  22372  icccmplem2  22434  icccmplem3  22435  reconnlem2  22438  metdscn  22467  cncfval  22499  elcncf2  22501  elcncf1di  22506  mulc1cncf  22516  cncfmet  22519  cnllycmp  22563  evth  22566  lebnumlem3  22570  lebnum  22571  xlebnum  22572  ishtpy  22579  isphtpy  22588  pi1xfr  22663  pi1coghm  22669  isclmp  22705  ipcn  22853  lmmbr2  22865  lmmbr3  22866  lmmbrf  22868  cfilfval  22870  iscfil  22871  fmcfil  22878  caufval  22881  iscau  22882  iscau2  22883  iscau3  22884  iscau4  22885  iscauf  22886  caucfil  22889  cfilresi  22901  causs  22904  lmclim  22909  cncmet  22927  cmetcusp1  22957  minveclem4c  23004  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  minveclem7  23014  ivthlem2  23028  ivthlem3  23029  cniccbdd  23037  ovolunlem1  23072  ovoliunlem1  23077  ovoliun2  23081  ovolicc2lem3  23094  ismbl  23101  ioombl1lem4  23136  uniioombllem2  23157  uniioombllem6  23162  dyadmax  23172  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  volcn  23180  ismbf1  23199  ismbf  23203  mbfeqalem  23215  mbfinf  23238  mbflimsup  23239  itg1climres  23287  mbfi1fseqlem6  23293  mbfi1flimlem  23295  itg2seq  23315  itg2monolem1  23323  itg2i1fseq  23328  itg2i1fseq2  23329  itg2cnlem1  23334  itg2cnlem2  23335  isibl  23338  dveflem  23546  ply1divex  23700  fta1g  23731  plyeq0lem  23770  dgrco  23835  plydivex  23856  fta1  23867  vieta1  23871  aannenlem1  23887  aannenlem2  23888  aalioulem2  23892  aalioulem3  23893  ulmval  23938  ulm2  23943  ulmi  23944  ulmres  23946  ulmshftlem  23947  ulmcaulem  23952  ulmcau  23953  ulmss  23955  ulmbdd  23956  ulmdvlem1  23958  ulmdvlem3  23960  mtestbdd  23963  iblulm  23965  abelthlem8  23997  pilem2  24010  pilem3  24011  divlogrlim  24181  cxpcn3  24289  dmarea  24484  rlimcnp  24492  cxplim  24498  cxploglim  24504  scvxcvx  24512  emcllem6  24527  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgambdd  24563  lgamcvglem  24566  ftalem1  24599  ftalem2  24600  ftalem3  24601  isppw2  24641  perfectlem2  24755  2sqlem6  24948  2sqlem10  24953  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  dchrisum0  25009  pntpbnd  25077  pntibndlem3  25081  pntibnd  25082  pntleme  25097  pntlem3  25098  pntlemp  25099  pnt3  25101  istrkgld  25158  axtg5seg  25164  tgcgr4  25226  perpln1  25405  perpln2  25406  isperp  25407  brbtwn2  25585  colinearalg  25590  axsegconlem1  25597  axsegcon  25607  ax5seglem4  25612  ax5seglem5  25613  axlowdim  25641  axeuclidlem  25642  axcontlem1  25644  axcontlem2  25645  axcontlem4  25647  axcontlem5  25648  axcontlem8  25651  axcontlem12  25655  cusgra3v  25993  wlks  26047  wlkcompim  26054  wlkelwrd  26058  wlkntrllem3  26091  constr3trllem2  26179  1conngra  26203  wwlk  26209  clwwlk  26294  isrgrac  26461  rusgra0edg  26482  iseupa  26492  frgrawopreg1  26577  frgrawopreg2  26578  frgrareg  26644  frgraregord013  26645  isgrpo  26735  isgrpoi  26736  grpoideu  26747  grpoidinv2  26753  vciOLD  26800  isvclem  26816  cnidOLD  26821  isnvlem  26849  nvi  26853  nmcvcn  26934  lnoval  26991  islno  26992  isblo3i  27040  blo3i  27041  blocnilem  27043  blocni  27044  ajfval  27048  ubthlem1  27110  ubthlem2  27111  ubthlem3  27112  ubth  27113  minvecolem2  27115  minvecolem3  27116  minvecolem4c  27119  minvecolem4  27120  minvecolem5  27121  minvecolem6  27122  minvecolem7  27123  htthlem  27158  h2hcau  27220  h2hlm  27221  hilid  27402  hcau  27425  hlimi  27429  hlim2  27433  ocel  27524  adjsym  28076  ellnop  28101  ellnfn  28126  hhcno  28147  hhcnf  28148  0cnop  28222  0cnfn  28223  idcnop  28224  lnopeq  28252  elunop2  28256  lnophm  28262  lnconi  28276  lnopcnbd  28279  lnfncnbd  28300  imaelshi  28301  riesz3i  28305  riesz4i  28306  riesz4  28307  riesz1  28308  cnlnadjlem2  28311  cnlnadjlem5  28314  cnlnadjlem8  28317  cnlnadji  28319  nmopadjlei  28331  cnvbraval  28353  leopg  28365  leoppos  28369  mdbr  28537  dmdbr  28542  cdj3i  28684  rmoeqALT  28711  disjunsn  28789  funcnv5mpt  28852  fgreu  28854  fcnvgreu  28855  xrge0infss  28915  resspos  28990  isomnd  29032  inftmrel  29065  isinftm  29066  archiabl  29083  rngurd  29119  isarchiofld  29148  crefeq  29240  rge0scvg  29323  qqhcn  29363  esumpcvgval  29467  esum2d  29482  sigaval  29500  issgon  29513  isrnmeas  29590  ismbfm  29641  isanmbfm  29645  mbfmcst  29648  elcarsg  29694  sitgval  29721  oddpwdc  29743  eulerpartlemd  29755  ballotleme  29885  signsw0g  29959  signswmnd  29960  bnj1185  30118  bnj1385  30157  bnj66  30184  bnj106  30192  bnj155  30203  bnj852  30245  bnj893  30252  bnj1228  30333  bnj1234  30335  bnj1463  30377  derangenlem  30407  subfacp1lem3  30418  subfacp1lem5  30420  subfacp1lem6  30421  subfacp1  30422  erdszelem8  30434  kur14  30452  cnpcon  30466  rescon  30482  cvmscbv  30494  iscvm  30495  cvmsi  30501  cvmsval  30502  cvmlift3lem2  30556  snmlval  30567  mclsssvlem  30713  mclsval  30714  mclsax  30720  mclsind  30721  dfpo2  30898  dfon2lem9  30940  dfrdg2  30945  dfrdg3  30946  poseq  30994  soseq  30995  frrlem1  31024  sltval  31044  nocvxminlem  31089  nobndlem2  31092  nobndlem8  31098  nobndup  31099  nobnddown  31100  fwddifnval  31440  nn0prpwlem  31487  isfne  31504  isfne4  31505  isfne2  31507  isfne3  31508  neibastop3  31527  topmeet  31529  topjoin  31530  filnetlem4  31546  dnicn  31652  unblimceq0lem  31667  unblimceq0  31668  unbdqndv2  31672  taupilemrplb  32343  csbwrecsg  32349  fin2so  32566  matunitlindflem2  32576  ptrecube  32579  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimirlem32  32611  poimir  32612  heicant  32614  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  voliunnfl  32623  volsupnfl  32624  mbfresfi  32626  itg2addnc  32634  ftc1anc  32663  f1opr  32689  upixp  32694  indexdom  32699  filbcmb  32705  sdclem2  32708  fdc  32711  lmclim2  32724  caures  32726  istotbnd  32738  istotbnd3  32740  sstotbnd  32744  isbnd  32749  heibor  32790  bfp  32793  rrncmslem  32801  exidu1  32825  cmpidelt  32828  exidres  32847  exidresid  32848  isrngod  32867  rngoideu  32872  isgrpda  32924  idlval  32982  isidl  32983  0idl  32994  unichnidl  33000  pridl  33006  ismaxidl  33009  smprngopr  33021  igenval2  33035  prnc  33036  ispridlc  33039  scottexf  33146  scott0f  33147  riotasvd  33260  islfl  33365  eqlkr  33404  eqlkr3  33406  glbconN  33681  hlsuprexch  33685  ispsubsp  34049  ldilset  34413  isldil  34414  dilsetN  34458  isdilN  34459  trlset  34466  trlval  34467  cdleme27b  34674  cdleme29b  34681  cdleme31so  34685  cdleme31sn1  34687  cdleme31sn1c  34694  cdleme31fv  34696  cdleme40v  34775  istendo  35066  cdlemkid3N  35239  cdlemkid4  35240  cdlemkid5  35241  dihfval  35538  dihval  35539  islpolN  35790  hdmapffval  36136  hdmapfval  36137  hdmapval  36138  hdmapval2lem  36141  hgmapffval  36195  hgmapfval  36196  hgmapval  36197  hgmapvs  36201  isnacs  36285  isnacs2  36287  nacsfix  36293  mzpclval  36306  elmzpcl  36307  rencldnfilem  36402  infmrgelbi  36460  pellfundre  36463  pellfundlb  36466  wepwsolem  36630  fnwe2lem2  36639  aomclem8  36649  dfac11  36650  gicabl  36687  islnr3  36704  hbtlem2  36713  hbtlem5  36717  fiinfi  36897  clsk1independent  37364  ntrclsk13  37389  gneispacess2  37464  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  evth2f  38197  ubelsupr  38202  evthf  38209  fnchoice  38211  uzwo4  38246  wessf1ornlem  38366  disjinfi  38375  dstregt0  38434  upbdrech2  38463  fiminre2  38535  mccl  38665  mullimc  38683  ellimcabssub0  38684  limcdm0  38685  climf  38689  mullimcf  38690  constlimc  38691  idlimc  38693  clim2f  38703  limsupre  38708  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  clim2cf  38717  clim0cf  38721  climf2  38733  clim2f2  38737  clim2d  38740  cncfshift  38759  cncfperiod  38764  fperdvper  38808  dvdivbd  38813  dvbdfbdioo  38820  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem3  38838  stoweidlem5  38898  stoweidlem9  38902  stoweidlem15  38908  stoweidlem16  38909  stoweidlem27  38920  stoweidlem28  38921  stoweidlem31  38924  stoweidlem34  38927  stoweidlem37  38930  stoweidlem46  38939  stoweidlem48  38941  stoweidlem51  38944  stoweidlem52  38945  stoweidlem59  38952  wallispilem3  38960  stirlinglem13  38979  fourierdlem2  39002  fourierdlem3  39003  fourierdlem16  39016  fourierdlem20  39020  fourierdlem21  39021  fourierdlem22  39022  fourierdlem25  39025  fourierdlem39  39039  fourierdlem42  39042  fourierdlem54  39053  fourierdlem64  39063  fourierdlem77  39076  fourierdlem83  39082  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  issal  39210  subsaliuncllem  39251  sge0supre  39282  sge0rnbnd  39286  ismea  39344  iundjiun  39353  meaiuninc2  39375  caragenval  39383  isome  39384  caragenel  39385  omessle  39388  ovnlerp  39452  hoidmvlelem1  39485  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvle  39490  issmflem  39613  issmfgt  39643  smfmullem2  39677  smfmullem4  39679  smfmul  39680  cbvral2  39821  raaan2  39824  2reu4a  39838  dfdfat2  39860  iccpart  39954  iccpartigtl  39961  perfectALTVlem2  40165  bgoldbachlt  40227  tgoldbachlt  40230  bgoldbachltOLD  40234  tgoldbachltOLD  40237  fpropnf1  40337  uvtxa01vtx0  40623  uvtxusgr  40629  iscusgredg  40645  rgrx0ndm  40793  ewlksfval  40803  1wlksfval  40811  wlksfval  40812  1wlkvtxedg  40852  wwlks  41038  1wlkiswwlks2  41072  clwwlks  41187  clwlkclwwlk  41211  clwlksfclwwlk  41269  1conngr  41361  frgrwopreg1  41487  frgrwopreg2  41488  av-frgraregord013  41549  mgmhmima  41592  rnghmval  41681  lidlmsgrp  41716  lidlrng  41717  zlidlring  41718  uzlidlring  41719  2zrngamnd  41731  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  linindslinci  42031  lindslinindsimp1  42040  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  linds0  42048  lindsrng01  42051  snlindsntor  42054  lmod1  42075  ldepsnlinc  42091  bigoval  42141  elbigo2r  42145  nn0sumshdiglem2  42214  setrec1lem2  42234