Theorem ralbidv 3120

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2108  ∀wral 3063

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  2ralbidv  3122  rexralbidv  3229  cbvral2vw  3385  cbvral2v  3388  rspceaimv  3557  rspc2  3560  rspc2v  3562  rspc3v  3565  reu6i  3658  reu7  3662  sbcralt  3801  reu8nf  3806  raaan  4448  raaanv  4449  raaan2  4452  2reu4lem  4453  reusngf  4605  2ralsng  4609  rexreusng  4612  reuprg0  4635  issn  4760  2ralunsn  4823  elintg  4884  elintrabg  4889  eliin  4926  disjprgw  5065  disjprg  5066  disjxun  5068  brralrspcev  5130  reusv2lem2  5317  reusv3  5323  poeq1  5497  solin  5519  somo  5531  frirr  5557  fr2nr  5558  frminex  5560  wereu2  5577  posn  5663  frsn  5665  ralxpf  5744  cnvpo  6179  reu3op  6184  reuop  6185  dfpo2  6188  frpomin  6228  fnmptfvd  6900  iinpreima  6928  dff4  6959  dff13f  7110  fpropnf1  7121  eusvobj2  7248  ovanraleqv  7279  f1opr  7309  ofreq  7515  sorpssuni  7563  sorpssint  7564  fr3nr  7600  onssmin  7619  funcnvuni  7752  f1oweALT  7788  frxp  7938  frecseq123  8069  csbfrecsg  8071  frrlem1  8073  frrlem13  8085  wrecseq123OLD  8102  wfrlem1OLD  8110  wfrlem3OLDa  8113  wfrlem15OLD  8125  smoeq  8152  tfrlem12  8191  tz7.48lem  8242  elixp2  8647  undifixp  8680  xpf1o  8875  nneneq  8896  ac6sfi  8988  frfi  8989  fipreima  9055  indexfi  9057  marypha1lem  9122  marypha1  9123  supeq1  9134  supeq3  9138  supmo  9141  eqsup  9145  supub  9148  suplub  9149  sup0  9155  supisoex  9163  eqinf  9173  infval  9175  infmo  9184  oieq1  9201  ordtypecbv  9206  ordtypelem3  9209  ordtypelem6  9212  ordtypelem7  9213  ordtypelem9  9215  wemaplem1  9235  wemaplem2  9236  zfregcl  9283  oemapval  9371  oemapvali  9372  cantnf  9381  wemapwe  9385  rankval3b  9515  unbndrank  9531  rankunb  9539  rankuni2b  9542  tcrank  9573  scottex  9574  scottexs  9576  scott0s  9577  bnd2  9582  updjud  9623  dfac8clem  9719  ac5num  9723  acni  9732  acni2  9733  alephval3  9797  dfac4  9809  dfac5lem5  9814  dfac5  9815  dfac2a  9816  dfac2b  9817  dfacacn  9828  kmlem2  9838  kmlem13  9849  cflem  9933  cflecard  9940  cfeq0  9943  cfsuc  9944  cfflb  9946  cofsmo  9956  cfsmolem  9957  cfcoflem  9959  coftr  9960  alephsing  9963  fin23lem11  10004  isfin3ds  10016  fin23lem17  10025  fin23lem39  10037  isf33lem  10053  isf34lem6  10067  fin1a2lem13  10099  hsmexlem4  10116  hsmex  10119  axcc2lem  10123  axcc3  10125  dcomex  10134  axdc2lem  10135  axdc3lem2  10138  axdc3lem3  10139  axdc3  10141  axdc4lem  10142  axcclem  10144  zorn2lem2  10184  zorn2lem7  10189  zorn2g  10190  zornn0g  10192  ttukeylem7  10202  axdclem2  10207  brdom3  10215  brdom7disj  10218  brdom6disj  10219  alephval2  10259  inar1  10462  axgroth6  10515  pinq  10614  nqereu  10616  prlem934  10720  supexpr  10741  supsrlem  10798  axpre-sup  10856  dedekind  11068  dedekindle  11069  fiminre2  11853  lbreu  11855  sup2  11861  infm3  11864  nnsub  11947  uzwo  12580  nnwof  12583  ublbneg  12602  lbzbi  12605  zsupss  12606  uzsupss  12609  uzwo3  12612  zmax  12614  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem4  12649  rpnnen1lem5  12650  xrsupsslem  12970  xrinfmsslem  12971  xrsupss  12972  xrinfmss  12973  flval2  13462  axdc4uzlem  13631  ssnn0fi  13633  fsuppmapnn0fiubex  13640  faclbnd4lem4  13938  bccl  13964  hashgt12el  14065  hashbc  14093  hashge2el2dif  14122  wrdind  14363  wrd2ind  14364  rexanre  14986  rexico  14993  cau4  14996  reusq0  15102  clim  15131  rlim  15132  rlim2  15133  clim2  15141  clim2c  15142  clim0c  15144  rlim0  15145  rlim0lt  15146  ello12r  15154  ello1d  15160  elo12r  15165  rlimresb  15202  rlimcld2  15215  climabs0  15222  rlimo1  15254  lo1add  15264  lo1mul  15265  isercoll  15307  incexclem  15476  sqrt2irr  15886  gcdcllem1  16134  gcdcllem2  16135  dfgcd2  16182  fissn0dvds  16252  dvdslcmf  16264  lcmfledvds  16265  lcmf  16266  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem  16274  lcmfdvds  16275  reumodprminv  16433  pc2dvds  16508  pcz  16510  prmpwdvds  16533  infpn2  16542  prmreclem2  16546  prmreclem3  16547  prmreclem5  16549  prmreclem6  16550  vdwlem6  16615  vdwlem8  16617  vdwlem13  16622  vdwnnlem1  16624  vdwnn  16627  ramcl  16658  cshwrepswhash1  16732  prdsleval  17105  imasval  17139  imasaddfnlem  17156  imasvscafn  17165  mrisval  17256  isacs  17277  isacs2  17279  isacs1i  17283  mreacs  17284  acsfn  17285  acsfn2  17289  iscatd  17299  catidex  17300  catideu  17301  cidval  17303  catidd  17306  comfeq  17332  catpropd  17335  ismon  17362  isfunc  17495  isnat  17579  isinito  17627  istermo  17628  isprs  17930  drsdirfi  17938  ispos  17947  lubfval  17983  lubeldm  17986  lubval  17989  lubprop  17991  lublecllem  17993  glbfval  17996  glbeldm  17999  glbval  18002  glbprop  18004  joinval2lem  18013  joinlem  18016  meetval2lem  18027  meetlem  18030  poslubmo  18044  posglbmo  18045  poslubd  18046  isglbd  18142  lubl  18145  lubun  18148  clatleglb  18151  isdlat  18155  ipodrsima  18174  mgm1  18257  gsumval2  18285  sgrp1  18299  mhmima  18378  mndind  18381  gsumwspan  18400  efmndmnd  18443  smndex1mnd  18464  sgrp2rid2  18480  sgrp2rid2ex  18481  sgrp2nmndlem4  18482  pwmnd  18491  dfgrp2  18519  isgrpinv  18547  grpidinv  18550  dfgrp3lem  18588  issubg4  18689  0subg  18695  isnsg2  18699  nsgacs  18705  elnmz  18706  cycsubgcl  18740  ghmrn  18762  ghmnsgima  18773  isga  18812  orbsta  18834  cntzfval  18841  elcntz  18843  resscntz  18853  oppgsubg  18885  symgextfo  18945  gsmsymgreqlem2  18954  gsmsymgreq  18955  pmtrdifel  19003  pmtrdifwrdellem3  19006  pmtrdifwrdel2  19009  psgnunilem2  19018  psgnunilem3  19019  odeq  19073  gexid  19101  gexlem2  19102  gexdvds  19104  isslw  19128  sylow2alem1  19137  sylow2alem2  19138  efgval  19238  efgrelexlemb  19271  efgcpbllemb  19276  abl1  19382  dmdprd  19516  dprd2da  19560  pgpfac1lem5  19597  ring1  19756  isabv  19994  islss  20111  lssacs  20144  reslmhm  20229  islbs  20253  pj1lmhm  20277  lbsacsbs  20333  isrrg  20472  zringlpir  20601  psgndiflemA  20718  ocvfval  20783  elocv  20785  iunocv  20798  frlmlbs  20914  islindf  20929  islinds2  20930  islindf2  20931  lindfrn  20938  lsslindf  20947  islindf4  20955  opsrval  21157  ply1coe  21377  cply1coe0bi  21381  mat0dimcrng  21527  mdetunilem1  21669  mdetunilem9  21677  cpmat  21766  cpmatel  21768  1elcpmat  21772  m2cpminvid2lem  21811  basgen2  22047  bastop1  22051  isclo  22146  ordtbaslem  22247  iscn  22294  cnpval  22295  iscnp  22296  iscnp3  22303  lmbr  22317  lmbr2  22318  lmbrf  22319  cnprest  22348  cnprest2  22349  t0sep  22383  isreg  22391  t1sep2  22428  tgcmp  22460  1stcclb  22503  1stcfb  22504  2ndc1stc  22510  1stcrest  22512  2ndcdisj  22515  islly  22527  isnlly  22528  lly1stc  22555  isref  22568  islocfin  22576  elkgen  22595  kgencn  22615  elpt  22631  elptr  22632  ptcnplem  22680  tx1stc  22709  cnmpt21  22730  kqt0lem  22795  isr0  22796  regr1lem2  22799  r0sep  22807  nrmr0reg  22808  flffbas  23054  cnflf  23061  cnflf2  23062  lmflf  23064  txflf  23065  fclsopni  23074  fclsnei  23078  fclsrest  23083  fcfnei  23094  cnfcf  23101  alexsubb  23105  alexsubALTlem3  23108  qustgplem  23180  tsmsfbas  23187  tsmsres  23203  tsmsf1o  23204  tsmsxplem1  23212  ustval  23262  isust  23263  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ust0  23279  utopval  23292  ucnval  23337  isucn  23338  isucn2  23339  ucnima  23341  iscfilu  23348  ispsmet  23365  ismet  23384  isxmet  23385  imasdsf1olem  23434  imasf1oxmet  23436  imasf1omet  23437  metss  23570  met1stc  23583  prdsxmslem2  23591  txmetcnp  23609  metucn  23633  tngngp3  23726  nlmvscn  23757  nmoval  23785  nmolb  23787  qtopbaslem  23828  cncfval  23957  elcncf2  23959  mulc1cncf  23974  cncfmet  23978  evth  24028  lebnumlem3  24032  lebnum  24033  xlebnum  24034  ishtpy  24041  isphtpy  24050  pi1xfr  24124  pi1coghm  24130  isclmp  24166  ipcn  24315  lmmbr2  24328  lmmbr3  24329  lmmbrf  24331  cfilfval  24333  iscfil  24334  fmcfil  24341  caufval  24344  iscau  24345  iscau2  24346  iscau3  24347  iscau4  24348  iscauf  24349  caucfil  24352  cfilresi  24364  causs  24367  lmclim  24372  cmetcusp1  24422  minveclem4c  24494  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem6  24503  minveclem7  24504  ovolicc2lem3  24588  ismbl  24595  dyadmax  24667  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  ismbf1  24693  ismbf  24697  mbfeqalem2  24711  mbflimsup  24735  mbfi1fseqlem6  24790  mbfi1flimlem  24792  itg2seq  24812  itg2monolem1  24820  isibl  24835  ply1divex  25206  fta1g  25237  dgrco  25341  plydivex  25362  fta1  25373  vieta1  25377  aannenlem1  25393  aannenlem2  25394  aalioulem2  25398  aalioulem3  25399  ulmval  25444  ulm2  25449  ulmi  25450  ulmres  25452  ulmshftlem  25453  ulmcaulem  25458  ulmcau  25459  ulmss  25461  ulmbdd  25462  ulmdvlem1  25464  ulmdvlem3  25466  pilem2  25516  pilem3  25517  cxpcn3  25806  dmarea  26012  rlimcnp  26020  scvxcvx  26040  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgambdd  26091  lgamcvglem  26094  isppw2  26169  perfectlem2  26283  2sqlem6  26476  2sqlem10  26481  addsq2reu  26493  2sqreulem1  26499  2sqreunnlem1  26502  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  pntpbnd  26641  pntibndlem3  26645  pntibnd  26646  pntleme  26661  pntlem3  26662  pntlemp  26663  pnt3  26665  istrkgld  26724  axtg5seg  26730  tgcgr4  26796  perpln1  26975  perpln2  26976  isperp  26977  brbtwn2  27176  colinearalg  27181  axsegconlem1  27188  axsegcon  27198  ax5seglem4  27203  ax5seglem5  27204  axlowdim  27232  axeuclidlem  27233  axcontlem1  27235  axcontlem2  27236  axcontlem4  27238  axcontlem5  27239  axcontlem8  27242  axcontlem12  27246  elntg2  27256  uvtxusgr  27672  rgrx0ndm  27863  ewlksfval  27871  wksfval  27879  wwlks  28101  wlkiswwlks2  28141  clwwlk  28248  1conngr  28459  frgrwopregasn  28581  frgrwopregbsn  28582  frgrwopreglem5ALT  28587  frgrregord013  28660  isgrpo  28760  isgrpoi  28761  grpoideu  28772  grpoidinv2  28778  vciOLD  28824  isvclem  28840  cnidOLD  28845  isnvlem  28873  nvi  28877  lnoval  29015  islno  29016  isblo3i  29064  blo3i  29065  blocnilem  29067  ajfval  29072  ubthlem1  29133  ubthlem2  29134  ubthlem3  29135  ubth  29136  minvecolem2  29138  minvecolem3  29139  minvecolem4c  29142  minvecolem4  29143  minvecolem5  29144  minvecolem6  29145  minvecolem7  29146  h2hcau  29242  h2hlm  29243  hilid  29424  hcau  29447  hlimi  29451  hlim2  29455  ocel  29544  adjsym  30096  ellnop  30121  ellnfn  30146  hhcno  30167  hhcnf  30168  lnopeq  30272  elunop2  30276  lnophm  30282  lnconi  30296  lnopcnbd  30299  lnfncnbd  30320  imaelshi  30321  riesz3i  30325  riesz4i  30326  riesz4  30327  riesz1  30328  cnlnadjlem2  30331  cnlnadjlem5  30334  cnlnadjlem8  30337  cnlnadji  30339  nmopadjlei  30351  cnvbraval  30373  leopg  30385  leoppos  30389  mdbr  30557  dmdbr  30562  cdj3i  30704  disjunsn  30834  funcnv5mpt  30907  fgreu  30911  fcnvgreu  30912  xrge0infss  30985  wrdt2ind  31127  resspos  31146  mgccole1  31170  mgccole2  31171  mgcmnt1  31172  mgcmnt2  31173  gsumhashmul  31218  isomnd  31229  inftmrel  31336  isinftm  31337  archiabl  31354  isarchiofld  31418  0nellinds  31468  lindssn  31475  elrspunidl  31508  prmidl  31517  ismxidl  31536  crefeq  31697  zarcmplem  31733  esum2d  31961  sigaval  31979  issgon  31991  isrnmeas  32068  ismbfm  32119  isanmbfm  32123  mbfmcst  32126  elcarsg  32172  sitgval  32199  eulerpartlemd  32233  ballotleme  32363  tgoldbachgt  32543  bnj1185  32673  bnj1385  32712  bnj66  32740  bnj106  32748  bnj155  32759  bnj852  32801  bnj893  32808  bnj1228  32891  bnj1234  32893  bnj1463  32935  nummin  32963  derangenlem  33033  subfacp1lem3  33044  subfacp1lem5  33046  subfacp1lem6  33047  subfacp1  33048  erdszelem8  33060  kur14  33078  cnpconn  33092  resconn  33108  cvmscbv  33120  iscvm  33121  cvmsi  33127  cvmsval  33128  cvmlift3lem2  33182  snmlval  33193  satfv1  33225  fmlasucdisj  33261  satffunlem1lem1  33264  satffunlem2lem1  33266  satfv1fvfmla1  33285  mclsssvlem  33424  mclsval  33425  mclsax  33431  mclsind  33432  dfon2lem9  33673  dfrdg2  33677  dfrdg3  33678  ttrcleq  33695  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  frxp2  33718  xpord2ind  33721  frxp3  33724  xpord3ind  33727  poseq  33729  soseq  33730  naddcllem  33758  naddov2  33761  sltval  33777  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupno  33833  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem5  33842  noinfcbv  33847  noinfno  33848  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noetalem1  33871  noetalem2  33872  nocvxminlem  33899  brsslt  33907  conway  33920  etasslt  33934  slerec  33940  madebdaylemlrcut  34006  madebday  34007  cofcutr  34019  lrrecfr  34027  fwddifnval  34392  nn0prpwlem  34438  isfne  34455  isfne4  34456  isfne2  34458  isfne3  34459  neibastop3  34478  topmeet  34480  topjoin  34481  filnetlem4  34497  unblimceq0lem  34613  unblimceq0  34614  unbdqndv2  34618  taupilemrplb  35418  fin2so  35691  lindsadd  35697  matunitlindflem2  35701  ptrecube  35704  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimirlem32  35736  poimir  35737  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  voliunnfl  35748  volsupnfl  35749  mbfresfi  35750  itg2addnc  35758  upixp  35814  indexdom  35819  filbcmb  35825  sdclem2  35827  fdc  35830  lmclim2  35843  caures  35845  istotbnd  35854  istotbnd3  35856  sstotbnd  35860  isbnd  35865  heibor  35906  bfp  35909  rrncmslem  35917  isgrpda  36040  idlval  36098  isidl  36099  0idl  36110  unichnidl  36116  pridl  36122  ismaxidl  36125  smprngopr  36137  igenval2  36151  prnc  36152  ispridlc  36155  scottexf  36253  scott0f  36254  riotasvd  36897  islfl  37001  eqlkr  37040  eqlkr3  37042  glbconN  37318  hlsuprexch  37322  ispsubsp  37686  ldilset  38050  isldil  38051  dilsetN  38094  isdilN  38095  trlset  38102  trlval  38103  cdleme27b  38309  cdleme29b  38316  cdleme31so  38320  cdleme31sn1  38322  cdleme31sn1c  38329  cdleme31fv  38331  cdleme40v  38410  istendo  38701  cdlemkid3N  38874  cdlemkid4  38875  cdlemkid5  38876  dihfval  39172  dihval  39173  islpolN  39424  hdmapffval  39767  hdmapfval  39768  hdmapval  39769  hdmapval2lem  39772  hgmapffval  39826  hgmapfval  39827  hgmapval  39828  hgmapvs  39832  sticksstones2  40031  qsalrel  40141  fsuppind  40202  sn-sup2  40360  isnacs  40442  isnacs2  40444  nacsfix  40450  mzpclval  40463  elmzpcl  40464  rencldnfilem  40558  infmrgelbi  40616  pellfundre  40619  pellfundlb  40622  wepwsolem  40783  fnwe2lem2  40792  aomclem8  40802  dfac11  40803  gicabl  40840  islnr3  40856  hbtlem2  40865  hbtlem5  40869  fiinfi  41069  clsk1independent  41545  ntrclsk13  41570  gneispacess2  41645  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2lem1  41669  imo72b2  41672  scottelrankd  41754  mnuop23d  41773  ismnushort  41808  evth2f  42447  evthf  42459  fnchoice  42461  uzwo4  42490  wessf1ornlem  42611  disjinfi  42620  rnmptlb  42677  rnmptbdd  42679  rnmptbd2  42684  rnmptbd  42691  dstregt0  42709  upbdrech2  42737  rexabslelem  42848  rexabsle  42849  uzub  42861  infrpgernmpt  42895  mccl  43029  ellimcabssub0  43048  climf  43053  clim2f  43067  limsupre  43072  clim2cf  43081  clim0cf  43085  climf2  43097  clim2f2  43101  clim2d  43104  limsupref  43116  limsupbnd1f  43117  climinf2  43138  limsuppnf  43142  climinfmpt  43146  climinf3  43147  limsupubuzmpt  43150  limsupmnf  43152  limsupre2lem  43155  limsupre2  43156  limsupmnfuzlem  43157  limsupmnfuz  43158  limsupre2mpt  43161  limsupre3lem  43163  limsupre3  43164  limsupre3mpt  43165  limsupre3uz  43167  limsupreuz  43168  limsupreuzmpt  43170  climuz  43175  liminfreuzlem  43233  liminfreuz  43234  cnrefiisplem  43260  xlimmnfvlem1  43263  xlimmnfv  43265  xlimpnfvlem1  43267  xlimpnfv  43269  xlimmnfmpt  43274  xlimpnfmpt  43275  cncfshift  43305  cncfperiod  43310  fperdvper  43350  dvbdfbdioo  43361  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem3  43379  stoweidlem5  43436  stoweidlem9  43440  stoweidlem15  43446  stoweidlem16  43447  stoweidlem27  43458  stoweidlem28  43459  stoweidlem31  43462  stoweidlem34  43465  stoweidlem37  43468  stoweidlem46  43477  stoweidlem48  43479  stoweidlem51  43482  stoweidlem52  43483  stoweidlem59  43490  wallispilem3  43498  stirlinglem13  43517  fourierdlem2  43540  fourierdlem3  43541  fourierdlem16  43554  fourierdlem20  43558  fourierdlem21  43559  fourierdlem22  43560  fourierdlem25  43563  fourierdlem39  43577  fourierdlem42  43580  fourierdlem54  43591  fourierdlem64  43601  fourierdlem77  43614  fourierdlem83  43620  fourierdlem103  43640  fourierdlem104  43641  subsaliuncllem  43786  iundjiun  43888  meaiunincf  43911  caragenval  43921  isome  43922  caragenel  43923  omessle  43926  ovnlerp  43990  hoidmvlelem3  44025  hoidmvle  44028  issmflem  44150  issmfgt  44179  smfmullem2  44213  smfmullem4  44215  smfmul  44216  smfsuplem2  44232  smfsup  44234  smfinflem  44237  smfinf  44238  cfsetsnfsetf  44439  cbvral2  44482  2reu8i  44492  2reuimp0  44493  dfdfat2  44507  iccpart  44756  iccpartigtl  44763  paireqne  44851  reupr  44862  perfectALTVlem2  45062  bgoldbachlt  45153  tgoldbachlt  45156  isomgreqve  45165  isomushgr  45166  isomuspgrlem2  45173  isomgrsym  45176  isomgrtr  45179  ushrisomgr  45181  upwlksfval  45185  mgmhmima  45244  nn0mnd  45261  lidlmsgrp  45372  lidlrng  45373  uzlidlring  45375  ply1mulgsumlem1  45615  ply1mulgsumlem2  45616  linindslinci  45677  lindslinindsimp1  45686  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  linds0  45694  lindsrng01  45697  snlindsntor  45700  lmod1  45721  ldepsnlinc  45737  bigoval  45783  elbigo2r  45787  nn0sumshdiglem2  45856  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  lubeldm2d  46140  glbeldm2d  46141  lubsscl  46142  glbsscl  46143  ipolubdm  46161  ipolub  46162  ipoglbdm  46164  ipoglb  46165  isthincd2lem2  46205  setrec1lem2  46280