Theorem ralbidv 3177

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 3175	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062

This theorem is referenced by:  2ralbidv  3218  rexralbidv  3220  3ralbidv  3221  4ralbidv  3222  cbvral2vw  3238  cbvral4vw  3241  cbvral2v  3364  rspceaimv  3616  rspc2  3619  rspc2v  3621  rspc3v  3626  rspc4v  3629  reu6i  3723  reu7  3727  sbcralt  3865  reu8nf  3870  raaan  4519  raaanv  4520  raaan2  4523  2reu4lem  4524  reusngf  4675  2ralsng  4679  rexreusng  4682  reuprg0  4705  issn  4832  2ralunsn  4894  elintg  4957  elintrabg  4964  eliin  5001  disjprgw  5142  disjprg  5143  disjxun  5145  brralrspcev  5207  reusv2lem2  5396  reusv3  5402  poeq1  5590  solin  5612  somo  5624  frirr  5652  fr2nr  5653  frminex  5655  wereu2  5672  posn  5759  frsn  5761  ralxpf  5844  cnvpo  6283  reu3op  6288  reuop  6289  dfpo2  6292  frpomin  6338  fnmptfvd  7039  iinpreima  7067  dff4  7099  dff13f  7251  fpropnf1  7262  eusvobj2  7397  ovanraleqv  7429  f1opr  7461  ofreq  7670  sorpssuni  7718  sorpssint  7719  fr3nr  7755  onssmin  7776  funcnvuni  7918  f1oweALT  7955  frxp  8108  frxp2  8126  xpord2indlem  8129  frxp3  8133  xpord3inddlem  8136  poseq  8140  soseq  8141  frecseq123  8263  csbfrecsg  8265  frrlem1  8267  frrlem13  8279  wrecseq123OLD  8296  wfrlem1OLD  8304  wfrlem3OLDa  8307  wfrlem15OLD  8319  smoeq  8346  tfrlem12  8385  tz7.48lem  8437  naddcllem  8671  naddov2  8674  naddunif  8688  naddasslem1  8689  naddasslem2  8690  elixp2  8891  undifixp  8924  xpf1o  9135  nneneq  9205  nneneqOLD  9217  ac6sfi  9283  frfi  9284  fipreima  9354  indexfi  9356  marypha1lem  9424  marypha1  9425  supeq1  9436  supeq3  9440  supmo  9443  eqsup  9447  supub  9450  suplub  9451  sup0  9457  supisoex  9465  eqinf  9475  infval  9477  infmo  9486  oieq1  9503  ordtypecbv  9508  ordtypelem3  9511  ordtypelem6  9514  ordtypelem7  9515  ordtypelem9  9517  wemaplem1  9537  wemaplem2  9538  zfregcl  9585  oemapval  9674  oemapvali  9675  cantnf  9684  wemapwe  9688  ttrcleq  9700  ttrcltr  9707  ttrclss  9711  ttrclselem2  9717  rankval3b  9817  unbndrank  9833  rankunb  9841  rankuni2b  9844  tcrank  9875  scottex  9876  scottexs  9878  scott0s  9879  bnd2  9884  updjud  9925  dfac8clem  10023  ac5num  10027  acni  10036  acni2  10037  alephval3  10101  dfac4  10113  dfac5lem5  10118  dfac5  10119  dfac2a  10120  dfac2b  10121  dfacacn  10132  kmlem2  10142  kmlem13  10153  cflem  10237  cflecard  10244  cfeq0  10247  cfsuc  10248  cfflb  10250  cofsmo  10260  cfsmolem  10261  cfcoflem  10263  coftr  10264  alephsing  10267  fin23lem11  10308  isfin3ds  10320  fin23lem17  10329  fin23lem39  10341  isf33lem  10357  isf34lem6  10371  fin1a2lem13  10403  hsmexlem4  10420  hsmex  10423  axcc2lem  10427  axcc3  10429  dcomex  10438  axdc2lem  10439  axdc3lem2  10442  axdc3lem3  10443  axdc3  10445  axdc4lem  10446  axcclem  10448  zorn2lem2  10488  zorn2lem7  10493  zorn2g  10494  zornn0g  10496  ttukeylem7  10506  axdclem2  10511  brdom3  10519  brdom7disj  10522  brdom6disj  10523  alephval2  10563  inar1  10766  axgroth6  10819  pinq  10918  nqereu  10920  prlem934  11024  supexpr  11045  supsrlem  11102  axpre-sup  11160  dedekind  11373  dedekindle  11374  fiminre2  12158  lbreu  12160  sup2  12166  infm3  12169  nnsub  12252  uzwo  12891  nnwof  12894  ublbneg  12913  lbzbi  12916  zsupss  12917  uzsupss  12920  uzwo3  12923  zmax  12925  rpnnen1lem1  12958  rpnnen1lem3  12959  rpnnen1lem4  12960  rpnnen1lem5  12961  xrsupsslem  13282  xrinfmsslem  13283  xrsupss  13284  xrinfmss  13285  flval2  13775  axdc4uzlem  13944  ssnn0fi  13946  fsuppmapnn0fiubex  13953  faclbnd4lem4  14252  bccl  14278  hashgt12el  14378  hashbc  14408  hashge2el2dif  14437  wrdind  14668  wrd2ind  14669  rexanre  15289  rexico  15296  cau4  15299  reusq0  15405  clim  15434  rlim  15435  rlim2  15436  clim2  15444  clim2c  15445  clim0c  15447  rlim0  15448  rlim0lt  15449  ello12r  15457  ello1d  15463  elo12r  15468  rlimresb  15505  rlimcld2  15518  climabs0  15525  rlimo1  15557  lo1add  15567  lo1mul  15568  isercoll  15610  incexclem  15778  sqrt2irr  16188  gcdcllem1  16436  gcdcllem2  16437  dfgcd2  16484  fissn0dvds  16552  dvdslcmf  16564  lcmfledvds  16565  lcmf  16566  lcmfunsnlem1  16570  lcmfunsnlem2lem1  16571  lcmfunsnlem  16574  lcmfdvds  16575  reumodprminv  16733  pc2dvds  16808  pcz  16810  prmpwdvds  16833  infpn2  16842  prmreclem2  16846  prmreclem3  16847  prmreclem5  16849  prmreclem6  16850  vdwlem6  16915  vdwlem8  16917  vdwlem13  16922  vdwnnlem1  16924  vdwnn  16927  ramcl  16958  cshwrepswhash1  17032  prdsleval  17419  imasval  17453  imasaddfnlem  17470  imasvscafn  17479  mrisval  17570  isacs  17591  isacs2  17593  isacs1i  17597  mreacs  17598  acsfn  17599  acsfn2  17603  iscatd  17613  catidex  17614  catideu  17615  cidval  17617  catidd  17620  comfeq  17646  catpropd  17649  ismon  17676  isfunc  17810  isnat  17894  isinito  17942  istermo  17943  isprs  18246  drsdirfi  18254  ispos  18263  lubfval  18299  lubeldm  18302  lubval  18305  lubprop  18307  lublecllem  18309  glbfval  18312  glbeldm  18315  glbval  18318  glbprop  18320  joinval2lem  18329  joinlem  18332  meetval2lem  18343  meetlem  18346  poslubmo  18360  posglbmo  18361  poslubd  18362  isglbd  18458  lubl  18461  lubun  18464  clatleglb  18467  isdlat  18471  ipodrsima  18490  mgm1  18573  gsumval2  18601  sgrp1  18616  mhmimalem  18701  mndind  18705  gsumwspan  18723  efmndmnd  18766  smndex1mnd  18787  sgrp2rid2  18803  sgrp2rid2ex  18804  sgrp2nmndlem4  18805  pwmnd  18814  dfgrp2  18843  isgrpinv  18874  grpidinv  18879  dfgrp3lem  18917  issubg4  19019  0subgOLD  19026  isnsg2  19030  nsgacs  19036  elnmz  19037  cycsubgcl  19077  ghmrn  19099  ghmnsgima  19110  isga  19149  orbsta  19171  cntzfval  19178  elcntz  19180  resscntz  19191  oppgsubg  19224  symgextfo  19284  gsmsymgreqlem2  19293  gsmsymgreq  19294  pmtrdifel  19342  pmtrdifwrdellem3  19345  pmtrdifwrdel2  19348  psgnunilem2  19357  psgnunilem3  19358  odeq  19412  gexid  19443  gexlem2  19444  gexdvds  19446  isslw  19470  sylow2alem1  19479  sylow2alem2  19480  efgval  19579  efgrelexlemb  19612  efgcpbllemb  19617  abl1  19728  dmdprd  19862  dprd2da  19906  pgpfac1lem5  19943  ring1  20115  lringuplu  20306  isabv  20419  islss  20537  lssacs  20570  reslmhm  20655  islbs  20679  pj1lmhm  20703  lbsacsbs  20761  isrrg  20896  zringlpir  21028  psgndiflemA  21145  ocvfval  21210  elocv  21212  iunocv  21225  frlmlbs  21343  islindf  21358  islinds2  21359  islindf2  21360  lindfrn  21367  lsslindf  21376  islindf4  21384  opsrval  21592  ply1coe  21811  cply1coe0bi  21815  mat0dimcrng  21963  mdetunilem1  22105  mdetunilem9  22113  cpmat  22202  cpmatel  22204  1elcpmat  22208  m2cpminvid2lem  22247  basgen2  22483  bastop1  22487  isclo  22582  ordtbaslem  22683  iscn  22730  cnpval  22731  iscnp  22732  iscnp3  22739  lmbr  22753  lmbr2  22754  lmbrf  22755  cnprest  22784  cnprest2  22785  t0sep  22819  isreg  22827  t1sep2  22864  tgcmp  22896  1stcclb  22939  1stcfb  22940  2ndc1stc  22946  1stcrest  22948  2ndcdisj  22951  islly  22963  isnlly  22964  lly1stc  22991  isref  23004  islocfin  23012  elkgen  23031  kgencn  23051  elpt  23067  elptr  23068  ptcnplem  23116  tx1stc  23145  cnmpt21  23166  kqt0lem  23231  isr0  23232  regr1lem2  23235  r0sep  23243  nrmr0reg  23244  flffbas  23490  cnflf  23497  cnflf2  23498  lmflf  23500  txflf  23501  fclsopni  23510  fclsnei  23514  fclsrest  23519  fcfnei  23530  cnfcf  23537  alexsubb  23541  alexsubALTlem3  23544  qustgplem  23616  tsmsfbas  23623  tsmsres  23639  tsmsf1o  23640  tsmsxplem1  23648  ustval  23698  isust  23699  ustincl  23703  ustdiag  23704  ustinvel  23705  ustexhalf  23706  ust0  23715  utopval  23728  ucnval  23773  isucn  23774  isucn2  23775  ucnima  23777  iscfilu  23784  ispsmet  23801  ismet  23820  isxmet  23821  imasdsf1olem  23870  imasf1oxmet  23872  imasf1omet  23873  metss  24008  met1stc  24021  prdsxmslem2  24029  txmetcnp  24047  metucn  24071  tngngp3  24164  nlmvscn  24195  nmoval  24223  nmolb  24225  qtopbaslem  24266  cncfval  24395  elcncf2  24397  mulc1cncf  24412  cncfmet  24416  evth  24466  lebnumlem3  24470  lebnum  24471  xlebnum  24472  ishtpy  24479  isphtpy  24488  pi1xfr  24562  pi1coghm  24568  isclmp  24604  ipcn  24754  lmmbr2  24767  lmmbr3  24768  lmmbrf  24770  cfilfval  24772  iscfil  24773  fmcfil  24780  caufval  24783  iscau  24784  iscau2  24785  iscau3  24786  iscau4  24787  iscauf  24788  caucfil  24791  cfilresi  24803  causs  24806  lmclim  24811  cmetcusp1  24861  minveclem4c  24933  minveclem2  24934  minveclem3b  24936  minveclem4  24940  minveclem6  24942  minveclem7  24943  ovolicc2lem3  25027  ismbl  25034  dyadmax  25106  dyadmbllem  25107  dyadmbl  25108  opnmbllem  25109  ismbf1  25132  ismbf  25136  mbfeqalem2  25150  mbflimsup  25174  mbfi1fseqlem6  25229  mbfi1flimlem  25231  itg2seq  25251  itg2monolem1  25259  isibl  25274  ply1divex  25645  fta1g  25676  dgrco  25780  plydivex  25801  fta1  25812  vieta1  25816  aannenlem1  25832  aannenlem2  25833  aalioulem2  25837  aalioulem3  25838  ulmval  25883  ulm2  25888  ulmi  25889  ulmres  25891  ulmshftlem  25892  ulmcaulem  25897  ulmcau  25898  ulmss  25900  ulmbdd  25901  ulmdvlem1  25903  ulmdvlem3  25905  pilem2  25955  pilem3  25956  cxpcn3  26245  dmarea  26451  rlimcnp  26459  scvxcvx  26479  lgamgulmlem2  26523  lgamgulmlem3  26524  lgamgulmlem5  26526  lgambdd  26530  lgamcvglem  26533  isppw2  26608  perfectlem2  26722  2sqlem6  26915  2sqlem10  26920  addsq2reu  26932  2sqreulem1  26938  2sqreunnlem1  26941  dchrisumlema  26980  dchrisumlem2  26982  dchrisumlem3  26983  pntpbnd  27080  pntibndlem3  27084  pntibnd  27085  pntleme  27100  pntlem3  27101  pntlemp  27102  pnt3  27104  sltval  27139  nosupprefixmo  27192  noinfprefixmo  27193  nosupcbv  27194  nosupno  27195  nosupdm  27196  nosupfv  27198  nosupres  27199  nosupbnd1lem1  27200  nosupbnd1lem3  27202  nosupbnd1lem5  27204  noinfcbv  27209  noinfno  27210  noinfdm  27211  noinffv  27213  noinfres  27214  noinfbnd1lem3  27217  noinfbnd1lem5  27219  noetalem1  27233  noetalem2  27234  nocvxminlem  27268  brsslt  27276  conway  27289  etasslt  27303  slerec  27309  madebdaylemlrcut  27382  madebday  27383  cofcutr  27400  lrrecfr  27416  addsprop  27449  negsunif  27518  istrkgld  27699  axtg5seg  27705  tgcgr4  27771  perpln1  27950  perpln2  27951  isperp  27952  brbtwn2  28152  colinearalg  28157  axsegconlem1  28164  axsegcon  28174  ax5seglem4  28179  ax5seglem5  28180  axlowdim  28208  axeuclidlem  28209  axcontlem1  28211  axcontlem2  28212  axcontlem4  28214  axcontlem5  28215  axcontlem8  28218  axcontlem12  28222  elntg2  28232  uvtxusgr  28648  rgrx0ndm  28839  ewlksfval  28847  wksfval  28855  wwlks  29078  wlkiswwlks2  29118  clwwlk  29225  1conngr  29436  frgrwopregasn  29558  frgrwopregbsn  29559  frgrwopreglem5ALT  29564  frgrregord013  29637  isgrpo  29737  isgrpoi  29738  grpoideu  29749  grpoidinv2  29755  vciOLD  29801  isvclem  29817  cnidOLD  29822  isnvlem  29850  nvi  29854  lnoval  29992  islno  29993  isblo3i  30041  blo3i  30042  blocnilem  30044  ajfval  30049  ubthlem1  30110  ubthlem2  30111  ubthlem3  30112  ubth  30113  minvecolem2  30115  minvecolem3  30116  minvecolem4c  30119  minvecolem4  30120  minvecolem5  30121  minvecolem6  30122  minvecolem7  30123  h2hcau  30219  h2hlm  30220  hilid  30401  hcau  30424  hlimi  30428  hlim2  30432  ocel  30521  adjsym  31073  ellnop  31098  ellnfn  31123  hhcno  31144  hhcnf  31145  lnopeq  31249  elunop2  31253  lnophm  31259  lnconi  31273  lnopcnbd  31276  lnfncnbd  31297  imaelshi  31298  riesz3i  31302  riesz4i  31303  riesz4  31304  riesz1  31305  cnlnadjlem2  31308  cnlnadjlem5  31311  cnlnadjlem8  31314  cnlnadji  31316  nmopadjlei  31328  cnvbraval  31350  leopg  31362  leoppos  31366  mdbr  31534  dmdbr  31539  cdj3i  31681  disjunsn  31812  funcnv5mpt  31880  fgreu  31884  fcnvgreu  31885  xrge0infss  31960  wrdt2ind  32104  resspos  32123  mgccole1  32147  mgccole2  32148  mgcmnt1  32149  mgcmnt2  32150  gsumhashmul  32195  isomnd  32206  inftmrel  32313  isinftm  32314  archiabl  32331  isarchiofld  32423  0nellinds  32471  lindssn  32482  elrspunidl  32534  prmidl  32546  ismxidl  32566  crefeq  32813  zarcmplem  32849  esum2d  33079  sigaval  33097  issgon  33109  isrnmeas  33186  ismbfm  33237  mbfmcst  33246  elcarsg  33292  sitgval  33319  eulerpartlemd  33353  ballotleme  33483  tgoldbachgt  33663  bnj1185  33792  bnj1385  33831  bnj66  33859  bnj106  33867  bnj155  33878  bnj852  33920  bnj893  33927  bnj1228  34010  bnj1234  34012  bnj1463  34054  nummin  34082  derangenlem  34150  subfacp1lem3  34161  subfacp1lem5  34163  subfacp1lem6  34164  subfacp1  34165  erdszelem8  34177  kur14  34195  cnpconn  34209  resconn  34225  cvmscbv  34237  iscvm  34238  cvmsi  34244  cvmsval  34245  cvmlift3lem2  34299  snmlval  34310  satfv1  34342  fmlasucdisj  34378  satffunlem1lem1  34381  satffunlem2lem1  34383  satfv1fvfmla1  34402  mclsssvlem  34541  mclsval  34542  mclsax  34548  mclsind  34549  dfon2lem9  34751  dfrdg2  34755  dfrdg3  34756  fwddifnval  35123  nn0prpwlem  35195  isfne  35212  isfne4  35213  isfne2  35215  isfne3  35216  neibastop3  35235  topmeet  35237  topjoin  35238  filnetlem4  35254  unblimceq0lem  35370  unblimceq0  35371  unbdqndv2  35375  taupilemrplb  36189  fin2so  36463  lindsadd  36469  matunitlindflem2  36473  ptrecube  36476  poimirlem2  36478  poimirlem3  36479  poimirlem4  36480  poimirlem24  36500  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  poimirlem28  36504  poimirlem29  36505  poimirlem30  36506  poimirlem32  36508  poimir  36509  heicant  36511  mblfinlem1  36513  mblfinlem2  36514  voliunnfl  36520  volsupnfl  36521  mbfresfi  36522  itg2addnc  36530  upixp  36585  indexdom  36590  filbcmb  36596  sdclem2  36598  fdc  36601  lmclim2  36614  caures  36616  istotbnd  36625  istotbnd3  36627  sstotbnd  36631  isbnd  36636  heibor  36677  bfp  36680  rrncmslem  36688  isgrpda  36811  idlval  36869  isidl  36870  0idl  36881  unichnidl  36887  pridl  36893  ismaxidl  36896  smprngopr  36908  igenval2  36922  prnc  36923  ispridlc  36926  scottexf  37024  scott0f  37025  disjsuc2  37249  riotasvd  37814  islfl  37918  eqlkr  37957  eqlkr3  37959  glbconN  38235  glbconNOLD  38236  hlsuprexch  38240  ispsubsp  38604  ldilset  38968  isldil  38969  dilsetN  39012  isdilN  39013  trlset  39020  trlval  39021  cdleme27b  39227  cdleme29b  39234  cdleme31so  39238  cdleme31sn1  39240  cdleme31sn1c  39247  cdleme31fv  39249  cdleme40v  39328  istendo  39619  cdlemkid3N  39792  cdlemkid4  39793  cdlemkid5  39794  dihfval  40090  dihval  40091  islpolN  40342  hdmapffval  40685  hdmapfval  40686  hdmapval  40687  hdmapval2lem  40690  hgmapffval  40744  hgmapfval  40745  hgmapval  40746  hgmapvs  40750  sticksstones2  40951  qsalrel  41059  fsuppind  41159  sn-sup2  41338  isnacs  41427  isnacs2  41429  nacsfix  41435  mzpclval  41448  elmzpcl  41449  rencldnfilem  41543  infmrgelbi  41601  pellfundre  41604  pellfundlb  41607  wepwsolem  41769  fnwe2lem2  41778  aomclem8  41788  dfac11  41789  gicabl  41826  islnr3  41842  hbtlem2  41851  hbtlem5  41855  onintunirab  41961  onsucf1lem  42004  cantnfresb  42059  safesnsupfilb  42154  rp-brsslt  42159  fiinfi  42309  clsk1independent  42782  ntrclsk13  42807  gneispacess2  42882  imo72b2lem0  42902  imo72b2lem2  42904  imo72b2lem1  42906  imo72b2  42909  scottelrankd  42991  mnuop23d  43010  ismnushort  43045  evth2f  43684  evthf  43696  fnchoice  43698  uzwo4  43725  wessf1ornlem  43867  disjinfi  43876  rnmptlb  43932  rnmptbdd  43934  rnmptbd2  43939  rnmptbd  43946  dstregt0  43977  upbdrech2  44004  rexabslelem  44114  rexabsle  44115  uzub  44127  infrpgernmpt  44161  mccl  44300  ellimcabssub0  44319  climf  44324  clim2f  44338  limsupre  44343  clim2cf  44352  clim0cf  44356  climf2  44368  clim2f2  44372  clim2d  44375  limsupref  44387  limsupbnd1f  44388  climinf2  44409  limsuppnf  44413  climinfmpt  44417  climinf3  44418  limsupubuzmpt  44421  limsupmnf  44423  limsupre2lem  44426  limsupre2  44427  limsupmnfuzlem  44428  limsupmnfuz  44429  limsupre2mpt  44432  limsupre3lem  44434  limsupre3  44435  limsupre3mpt  44436  limsupre3uz  44438  limsupreuz  44439  limsupreuzmpt  44441  climuz  44446  liminfreuzlem  44504  liminfreuz  44505  cnrefiisplem  44531  xlimmnfvlem1  44534  xlimmnfv  44536  xlimpnfvlem1  44538  xlimpnfv  44540  xlimmnfmpt  44545  xlimpnfmpt  44546  cncfshift  44576  cncfperiod  44581  fperdvper  44621  dvbdfbdioo  44632  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  dvnprodlem3  44650  stoweidlem5  44707  stoweidlem9  44711  stoweidlem15  44717  stoweidlem16  44718  stoweidlem27  44729  stoweidlem28  44730  stoweidlem31  44733  stoweidlem34  44736  stoweidlem37  44739  stoweidlem46  44748  stoweidlem48  44750  stoweidlem51  44753  stoweidlem52  44754  stoweidlem59  44761  wallispilem3  44769  stirlinglem13  44788  fourierdlem2  44811  fourierdlem3  44812  fourierdlem16  44825  fourierdlem20  44829  fourierdlem21  44830  fourierdlem22  44831  fourierdlem25  44834  fourierdlem39  44848  fourierdlem42  44851  fourierdlem54  44862  fourierdlem64  44872  fourierdlem77  44885  fourierdlem83  44891  fourierdlem103  44911  fourierdlem104  44912  subsaliuncllem  45059  iundjiun  45162  meaiunincf  45185  caragenval  45195  isome  45196  caragenel  45197  omessle  45200  ovnlerp  45264  hoidmvlelem3  45299  hoidmvle  45302  issmflem  45429  issmfgt  45458  smfmullem2  45494  smfmullem4  45496  smfmul  45497  smfsuplem2  45514  smfsup  45516  smfinflem  45519  smfinf  45520  fsupdm  45544  finfdm  45548  cfsetsnfsetf  45754  cbvral2  45797  2reu8i  45807  2reuimp0  45808  dfdfat2  45822  iccpart  46070  iccpartigtl  46077  paireqne  46165  reupr  46176  perfectALTVlem2  46376  bgoldbachlt  46467  tgoldbachlt  46470  isomgreqve  46479  isomushgr  46480  isomuspgrlem2  46487  isomgrsym  46490  isomgrtr  46493  ushrisomgr  46495  upwlksfval  46499  mgmhmima  46558  nn0mnd  46575  rngisomring  46704  rhmimasubrnglem  46728  rnglidlmcl  46732  rnglidl0  46734  uzlidlring  46780  ply1mulgsumlem1  47020  ply1mulgsumlem2  47021  linindslinci  47082  lindslinindsimp1  47091  lindslinindsimp2lem5  47096  lindslinindsimp2  47097  linds0  47099  lindsrng01  47102  snlindsntor  47105  lmod1  47126  ldepsnlinc  47142  bigoval  47188  elbigo2r  47192  nn0sumshdiglem2  47261  eenglngeehlnmlem1  47376  eenglngeehlnmlem2  47377  lubeldm2d  47544  glbeldm2d  47545  lubsscl  47546  glbsscl  47547  ipolubdm  47565  ipolub  47566  ipoglbdm  47568  ipoglb  47569  isthincd2lem2  47609  setrec1lem2  47686