Theorem rexbidv 3179

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.)

Hypothesis

Ref	Expression
ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 482	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rexbidva 3177	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  ∃wrex 3071

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 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  2rexbidv  3220  rexralbidv  3221  cbvrex2vw  3240  cbvrex2v  3366  rspc2ev  3624  rspc3ev  3628  ceqsrex2v  3646  reuxfr1d  3746  uniiunlem  4084  n0snor2el  4834  eliun  5001  dfiun2g  5033  dfiin2g  5035  dfiunv2  5038  dmopab2rex  5916  elrnmpt  5954  elrnmptg  5957  elimag  6062  fvelrnb  6950  fvelimab  6962  foelrn  7105  foco2  7106  elabrex  7239  abrexco  7240  f1oiso  7345  f1oiso2  7346  orduninsuc  7829  funcnvuni  7919  fiunlem  7925  fiun  7926  f1iun  7927  abrexex2g  7948  f1oweALT  7956  el2xptp  8018  orderseqlem  8140  poseq  8141  soseq  8142  tfrlem12  8386  seqomlem2  8448  nneob  8652  eldifsucnn  8660  coflton  8667  cofon1  8668  cofon2  8669  naddunif  8689  qseq2  8755  elqsg  8759  elqsecl  8762  elixpsn  8928  ixpsnf1o  8929  isfi  8969  pssnn  9165  enfiALT  9188  pssnnOLD  9262  frfi  9285  unblem1  9292  unblem2  9293  unbnn2  9297  fofinf1o  9324  finsschain  9356  indexfi  9357  elfi  9405  marypha1lem  9425  supeq3  9441  supmo  9444  suplub  9452  supisolem  9465  eqinf  9476  infval  9478  infglb  9482  infglbb  9483  infmo  9487  oieq1  9504  ordtypelem2  9511  ordtypelem3  9512  ordtypelem9  9518  wemaplem1  9538  brwdom2  9565  brwdom3  9574  unwdomg  9576  oemapval  9675  cantnf  9685  wemapwe  9689  cnfcom3clem  9697  ttrcleq  9701  brttrcl  9705  ttrcltr  9708  tz9.13  9783  tz9.13g  9784  cardf2  9935  isnum2  9937  ennum  9939  cardiun  9974  infxpenc2  10014  aceq1  10109  aceq2  10111  dfac5lem3  10117  dfac5lem4  10118  dfac2a  10121  dfac2b  10122  kmlem9  10150  kmlem12  10153  kmlem14  10155  ackbij1  10230  cflm  10242  cfss  10257  cofsmo  10261  cfsmolem  10262  cfcoflem  10264  coftr  10265  isfin7  10293  fin23lem26  10317  isf32lem5  10349  fin1a2lem11  10402  hsmexlem2  10419  axdc3lem3  10444  axdc3  10446  numthcor  10486  zorn2lem7  10494  brdom3  10520  brdom7disj  10523  brdom6disj  10524  iundom2g  10532  fpwwe2  10635  winainflem  10685  winalim2  10688  inar1  10767  tskuni  10775  nqereu  10921  prnmax  10987  genpv  10991  genpnmax  10999  genpass  11001  prlem936  11039  recexsrlem  11095  map2psrpr  11102  supsrlem  11103  axrrecex  11155  axpre-sup  11161  dedekind  11374  cnegex  11392  recex  11843  fimaxre3  12157  infm3  12170  supaddc  12178  supadd  12179  supmul1  12180  supmullem1  12181  supmullem2  12182  supmul  12183  creur  12203  creui  12204  cju  12205  nnunb  12465  arch  12466  xrsupsslem  13283  xrinfmsslem  13284  xrsupss  13285  xrinfmss  13286  xrub  13288  supxrunb1  13295  supxrunb2  13296  infmremnf  13319  infmrp1  13320  modmuladd  13875  fsequb2  13938  hashge2el2difr  14439  iswrd  14463  wrdval  14464  csbwrdg  14491  cshword  14738  0csh0  14740  2cshwcshw  14773  scshwfzeqfzo  14774  cshimadifsn  14777  shftfval  15014  abs1m  15279  rexfiuz  15291  reusq0  15406  limsupbnd2  15424  clim  15435  rlim  15436  rlim2  15437  rlim0  15449  rlim0lt  15450  ello1mpt2  15463  o1lo1  15478  o1compt  15528  rlimdiv  15589  climsup  15613  sumeq1  15632  sumeq2w  15635  summo  15660  fsum  15663  fsumcvg3  15672  infcvgaux2i  15801  mertenslem1  15827  mertenslem2  15828  mertens  15829  prodeq1f  15849  prodeq2w  15853  prodmo  15877  fprod  15882  divides  16196  odd2np1lem  16280  opeo  16305  omeo  16306  divalglem4  16336  divalglem10  16342  divalg  16343  gcdcllem3  16439  zeqzmulgcd  16448  bezoutlem1  16478  exprmfct  16638  nnnn0modprm0  16736  pythagtriplem2  16747  pythagtrip  16764  pceu  16776  pcprmpw2  16812  unbenlem  16838  4sqlem12  16886  vdwapval  16903  vdwapun  16904  vdwmc2  16909  vdwpc  16910  vdwlem2  16912  vdwlem10  16920  vdwlem13  16923  vdwnnlem1  16925  rami  16945  cshwsiun  17030  cshwrepswhash1  17033  brssc  17758  cat1  18044  isdrs  18251  drsdir  18252  drsdirfi  18255  isdrs2  18256  ipodrsima  18491  grprinvlem  18589  gsumvalx  18592  gsumpropd  18594  gsumress  18598  isnsgrp  18611  smndex2dnrinv  18793  sgrp2nmndlem5  18807  grpinvex  18826  dfgrp2  18844  grpidinv2  18879  grpidinv  18880  dfgrp3lem  18918  grp1  18927  imasgrp2  18935  cyccom  19075  conjnmzb  19122  gaorb  19166  orbsta  19172  symgfix2  19279  symgextfo  19285  pmtrprfvalrn  19351  psgnunilem3  19359  psgneu  19369  psgnval  19370  psgnvali  19371  psgnvalii  19372  ispgp  19455  subgpgp  19460  sylow1  19466  pgpfi  19468  sylow2blem3  19485  fislw  19488  sylow3lem2  19491  lsmelvalm  19514  lsmass  19532  pj1fval  19557  pj1val  19558  pj1eu  19559  pj1id  19562  efgrelexlema  19612  efgrelexlemb  19613  efgredeu  19615  cyggeninv  19746  pgpfac1lem2  19940  pgpfac1lem3  19942  pgpfac1lem4  19943  pgpfac1  19945  pgpfaclem2  19947  pgpfac  19949  dvdsrval  20168  dvdsr  20169  subrgdvds  20370  lss1d  20567  lspsn  20606  lspsnel  20607  lspsolvlem  20748  rspsn  20885  znf1o  21099  cygznlem3  21117  psgndiflemA  21146  ellspd  21349  opsrval  21593  mat1dimelbas  21965  mat1dimbas  21966  scmatval  21998  scmatel  21999  scmateALT  22006  mat0scmat  22032  decpmataa0  22262  decpmatmulsumfsupp  22267  pmatcollpw2lem  22271  pm2mpmhmlem1  22312  chpscmat  22336  basis2  22446  eltg2  22453  tg2  22460  isclo  22583  neival  22598  isnei  22599  isneip  22601  restbas  22654  neitr  22676  cnpval  22732  iscnp  22733  cnpimaex  22752  lmbr  22754  lmbr2  22755  cnprest2  22786  lmff  22797  regsep  22830  pnrmopn  22839  nrmsep3  22851  isnrm2  22854  iscmp  22884  cmpsublem  22895  cmpsub  22896  tgcmp  22897  sscmp  22901  hauscmplem  22902  1stcclb  22940  1stcfb  22941  is2ndc  22942  2ndc1stc  22947  1stcrest  22949  2ndcctbss  22951  1stcelcls  22957  llyeq  22966  nllyeq  22967  hausllycmp  22990  lly1stc  22992  refssex  23007  refun0  23011  islocfin  23013  locfinnei  23019  comppfsc  23028  txbas  23063  ptval  23066  ptpjopn  23108  ptclsg  23111  txcnp  23116  ptcnp  23118  txrest  23127  ptrescn  23135  txcmp  23139  tx1stc  23146  xkococn  23156  kqreglem1  23237  fbasssin  23332  fbssfi  23333  fbssint  23334  fbun  23336  fgss2  23370  fgcl  23374  ufli  23410  fmfnfmlem3  23452  fbflim2  23473  hauspwpwf1  23483  flfneii  23488  flftg  23492  txflf  23502  fclscf  23521  alexsubb  23542  alexsubALT  23547  tsmssubm  23639  ustincl  23704  ustdiag  23705  ustinvel  23706  ustexhalf  23707  ust0  23716  trust  23726  elutop  23730  ucnval  23774  ucncn  23782  cfiluexsm  23787  cfiluweak  23792  blssps  23922  blss  23923  imasf1oxms  23990  mopni  23993  metss  24009  metrest  24025  metcnp3  24041  cfilucfil  24060  metuel2  24066  nlmvscn  24196  nrginvrcn  24201  icccmplem1  24330  icccmplem2  24331  icccmp  24333  divcn  24376  cncfval  24396  elcncf2  24398  cncfmet  24417  cnheibor  24463  evth  24467  lebnumlem3  24471  lebnum  24472  xlebnum  24473  lebnumii  24474  ipcn  24755  lmmbr  24767  lmmbr2  24768  cfilfval  24773  cfili  24777  iscfil3  24782  caufval  24784  iscau  24785  iscau2  24786  equivcfil  24808  equivcau  24809  lmcau  24822  ovolval  24982  elovolm  24984  ovolgelb  24989  ovoliunlem1  25011  ovoliun2  25015  ovolshftlem1  25018  ovolscalem1  25022  ovolicc  25032  ioombl1lem4  25070  uniioombllem2  25092  mbfaddlem  25169  mbfsup  25173  mbfinf  25174  mbflimsup  25175  i1fmulc  25213  itg1climres  25224  itg2val  25238  itg2l  25239  itg2leub  25244  itg2seq  25252  itg2monolem1  25260  itg2mono  25263  itg2i1fseq2  25266  cniccibl  25350  cnicciblnc  25352  ellimc3  25388  limciun  25403  dvferm1  25494  dvferm2  25496  lhop1lem  25522  ply1divex  25646  ig1peu  25681  plyval  25699  elply2  25702  coeval  25729  coeeu  25731  coelem  25732  coeeq  25733  plydivlem4  25801  plydivex  25802  aannenlem2  25834  aalioulem2  25838  aaliou2  25845  ulmval  25884  ulm2  25889  ulmcau  25899  ulmdvlem3  25906  abelthlem9  25944  abelth  25945  efif1olem4  26046  eflogeq  26102  efopn  26158  cxpcn3  26246  cxpeq  26255  rlimcnp  26460  lgamgulmlem6  26528  muval  26626  dchrptlem1  26757  dchrptlem2  26758  lgsdchrval  26847  2lgslem1b  26885  addsq2nreurex  26937  pntpbnd  27081  pntibndlem3  27085  pntibnd  27086  pntlemi  27097  pntleme  27101  pntlemp  27103  pnt3  27105  elno  27139  sltval  27140  nosupprefixmo  27193  noinfprefixmo  27194  nosupcbv  27195  nosupno  27196  nosupdm  27197  nosupfv  27199  nosupres  27200  nosupbnd1lem1  27201  nosupbnd1lem3  27203  nosupbnd1lem4  27204  nosupbnd1lem5  27205  noinfcbv  27210  noinfno  27211  noinfdm  27212  noinffv  27214  noinfres  27215  noinfbnd1lem3  27218  noinfbnd1lem4  27219  noinfbnd1lem5  27220  madef  27341  cofsslt  27395  coinitsslt  27396  cofss  27407  coiniss  27408  addsval  27436  addsval2  27437  addsproplem2  27444  addsproplem4  27446  addsproplem5  27447  addsproplem6  27448  addscut  27452  sleadd1  27462  addsuniflem  27474  addsunif  27475  addsasslem1  27476  addsasslem2  27477  negsid  27505  negsunif  27519  mulsval  27555  mulsuniflem  27594  addsdilem1  27596  mulsasslem1  27608  precsexlemcbv  27642  precsexlem3  27645  precsexlem8  27650  precsexlem9  27651  precsexlem11  27653  precsex  27654  istrkgld  27700  istrkg3ld  27702  axtgsegcon  27705  axtgpasch  27708  axtgcont1  27709  axtgupdim2  27712  legov  27826  islnopp  27980  ishpg  28000  hpgbr  28001  hpgcom  28008  iscgra1  28051  isinag  28079  isleag  28088  ttgval  28116  ttgvalOLD  28117  ttgitvval  28129  ttgelitv  28130  brbtwn  28147  brcgr  28148  axpasch  28189  axlowdim2  28208  axlowdim  28209  axcontlem2  28213  axcontlem4  28215  axcontlem7  28218  axcontlem8  28219  upgredg2vtx  28391  edglnl  28393  usgredg4  28464  ushgredgedg  28476  ushgredgedgloop  28478  dfnbgr2  28584  nbgrel  28587  nbumgrvtx  28593  nbgrnself  28606  uvtxel1  28643  cusgrfilem2  28703  cusgrfi  28705  vtxd0nedgb  28735  fusgrn0degnn0  28746  wlkonl1iedg  28912  wspniunwspnon  29167  elwwlks2on  29203  clwwlknscsh  29305  erclwwlkneq  29310  eleclclwwlkn  29319  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  3cyclfrgrrn1  29528  friendshipgt3  29641  isgrpo  29738  isgrpoi  29739  grpoidinvlem3  29747  grpoideu  29750  grpoidinv2  29756  nmoofval  30003  nmooval  30004  nmosetn0  30006  nmoolb  30012  nmoubi  30013  nmlno0lem  30034  chcompl  30483  pjhthmo  30543  pjhval  30638  pjpreeq  30639  h1de2ci  30797  elspansn  30807  nmopval  31097  nmopsetn0  31106  nmfnval  31117  nmfnsetn0  31119  eigvecval  31137  hhcno  31145  hhcnf  31146  nmoplb  31148  nmopub  31149  nmfnlb  31165  nmfnleub  31166  eleigvec  31198  nmlnop0iALT  31236  nmopun  31255  nmcexi  31267  branmfn  31346  pjnmopi  31389  cvbr  31523  hatomic  31601  chrelat2  31611  cdjreui  31673  cdj3lem2  31676  elabreximd  31735  br8d  31827  unipreima  31857  abfmpunirn  31865  curry2ima  31918  toslublem  32130  tosglblem  32132  cyc3genpm  32299  archirng  32322  archiexdiv  32324  archiabllem2a  32328  archiabl  32332  isarchiofld  32424  elgrplsmsn  32489  lsmssass  32501  grplsm0l  32502  grplsmid  32503  mxidlprm  32575  fedgmul  32705  ccfldextdgrr  32735  crefi  32816  pcmplfin  32829  rspectopn  32836  pstmfval  32865  tpr2rico  32881  rge0scvg  32918  ismntop  32995  esumc  33038  esumpcvgval  33065  esum2dlem  33079  inelsros  33165  diffiunisros  33166  dya2icoseg2  33266  dya2iocuni  33271  eulerpartlemgvv  33364  eulerpartlemgh  33366  hgt749d  33650  tgoldbachgt  33664  bnj66  33860  bnj873  33924  bnj18eq1  33927  bnj1234  34013  bnj1318  34025  cplgredgex  34100  subfacp1lem3  34162  pconncn  34204  cnpconn  34210  txpconn  34212  connpconn  34215  iscvm  34239  cvmcov  34243  cvmopnlem  34258  cvmliftlem15  34278  cvmlift3lem2  34300  cvmlift3lem4  34302  cvmlift3  34308  satf  34333  satfv1  34343  satfvsucsuc  34345  satfbrsuc  34346  satfrnmapom  34350  satf0op  34357  sat1el2xp  34359  fmlafvel  34365  fmlasuc  34366  fmla1  34367  isfmlasuc  34368  fmlaomn0  34370  fmlasucdisj  34379  satffunlem1lem1  34382  satffunlem1lem2  34383  satffunlem2lem1  34384  dmopab3rexdif  34385  satffunlem2lem2  34386  sategoelfvb  34399  satfv1fvfmla1  34403  2goelgoanfmla1  34404  br8  34715  br6  34716  br4  34717  dfrdg2  34756  dfrdg3  34757  altxpeq2  34935  funtransport  34992  fvtransport  34993  brcolinear2  35019  colineardim1  35022  segcon2  35066  brsegle  35069  funray  35101  fvray  35102  funline  35103  linedegen  35104  fvline  35105  ellines  35113  gg-divcn  35152  nn0prpwlem  35196  fnessref  35231  neibastop2lem  35234  neibastop2  35235  tailfb  35251  unblimceq0lem  35371  unblimceq0  35372  unbdqndv2  35376  bj-finsumval0  36155  relowlssretop  36233  nlpineqsn  36278  pibp19  36284  phpreu  36461  matunitlindflem2  36474  ptrest  36476  poimirlem4  36481  poimirlem17  36494  poimirlem20  36497  poimirlem24  36501  poimirlem26  36503  poimirlem27  36504  poimirlem28  36505  poimirlem31  36508  poimirlem32  36509  poimir  36510  heicant  36512  mblfinlem1  36514  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnclem  36528  itg2addnclem3  36530  itg2addnc  36531  itg2gt0cn  36532  ftc1anclem6  36555  unirep  36571  indexa  36590  sdclem2  36599  sdclem1  36600  sdc  36601  fdc  36602  fdc1  36603  incsequz  36605  istotbnd  36626  sstotbnd2  36631  equivtotbnd  36635  isbnd  36637  bndss  36643  ssbnd  36645  totbndbnd  36646  ismtybndlem  36663  heibor1lem  36666  heiborlem1  36668  heiborlem6  36673  heiborlem8  36675  heiborlem10  36677  heibor  36678  rngoid  36759  isgrpda  36812  isdrngo2  36815  divrngidl  36885  prnc  36924  isfldidl  36925  exanres3  37154  brcoels  37294  br1cossxrnres  37307  eldm1cossres2  37320  prtlem5  37719  prtlem13  37727  prtlem16  37728  islshp  37838  lsmsat  37867  lcvbr  37880  lsatcv0  37890  lshpsmreu  37968  lshpkrlem1  37969  lshpkrlem2  37970  lshpkrlem3  37971  lshpkrcl  37975  lshpset2N  37978  islshpkrN  37979  cvrval  38128  atlex  38175  glbconxN  38238  hlsuprexch  38241  islln  38366  islpln  38390  islpln5  38395  lvolex3N  38398  islvol  38433  islvol5  38439  ispointN  38602  pmapglbx  38629  paddval  38658  elpaddn0  38660  elpaddat  38664  elpadd0  38669  4atex  38936  4atex2  38937  cdlemefrs29bpre1  39257  cdlemefrs32fva  39260  cdlemg33b  39567  dvhb1dimN  39846  dvhopellsm  39977  dib1dim  40025  diclspsn  40054  dihglblem2aN  40153  dihglblem2N  40154  dih1dimatlem  40189  dvh3dimatN  40299  dvh2dim  40305  dvh3dim  40306  dvh4dimN  40307  dvh3dim3N  40309  dochfl1  40336  lcfl7N  40361  lcf1o  40411  lcfrlem39  40441  mapdpglem3  40535  hvmapvalvalN  40621  hdmap14lem2a  40727  hdmapglem7a  40787  3factsumint1  40875  aks6d1c2p2  40946  3rspcedvd  41028  nnn1suc  41178  prjspeclsp  41351  elrfi  41418  isnacs  41428  nacsfg  41429  nacsfix  41436  mzpcompact2lem  41475  eldiophb  41481  eldioph  41482  eldioph2  41486  eldioph2b  41487  eldioph3  41490  eldiophss  41498  diophrex  41499  sbcrexgOLD  41509  sbc2rexgOLD  41512  rexrabdioph  41518  rexfrabdioph  41519  elnn0rabdioph  41527  dvdsrabdioph  41534  eldioph4b  41535  eldioph4i  41536  diophren  41537  rencldnfilem  41544  pell1234qrdich  41585  jm2.27  41733  expdiophlem1  41746  wepwsolem  41770  aomclem8  41789  islnr3  41843  lnr2i  41844  lpirlnr  41845  hbtlem1  41851  hbtlem2  41852  hbtlem7  41853  hbtlem4  41854  hbtlem5  41856  hbtlem6  41857  dgraaval  41872  dgraalem  41873  dgraaub  41876  rngunsnply  41901  onsupmaxb  41974  onexoegt  41979  onsucelab  41999  limnsuc  42001  oaordnr  42032  omnord1  42041  oenord1  42052  oaomoencom  42053  oenass  42055  cantnfresb  42060  tfsconcatfv2  42076  tfsconcatb0  42080  tfsconcat0i  42081  ofoafo  42092  naddcnffo  42100  oaun3lem1  42110  oadif1lem  42115  oadif1  42116  minregex2  42272  brtrclfv2  42464  clsk1indlem1  42782  extoimad  42902  mnuop123d  43007  mnuop23d  43011  mnuprdlem1  43017  mnuprdlem2  43018  ismnushort  43046  elabrexg  43714  foelrnf  43870  disjrnmpt2  43872  upbdrech  44002  ssfiunibd  44006  supxrgere  44030  supxrgelem  44034  supxrge  44035  suplesup  44036  infxr  44064  infleinf  44069  supxrunb3  44096  unb2ltle  44112  uzub  44128  supminfxr  44161  iccshift  44218  iooshift  44222  climinf  44309  climinff  44314  ellimcabssub0  44320  climf  44325  limcperiod  44331  limclner  44354  climf2  44369  clim2d  44376  limsuppnfd  44405  limsuppnf  44414  climinfmpt  44418  limsupubuzmpt  44422  limsupmnf  44424  limsupre2lem  44427  limsupre2  44428  limsupmnfuz  44430  limsupre2mpt  44433  limsupre3lem  44435  limsupre3  44436  limsupre3mpt  44437  limsupre3uzlem  44438  limsupre3uz  44439  limsupreuz  44440  limsupreuzmpt  44442  climuz  44447  liminfreuzlem  44505  liminfreuz  44506  xlimmnfvlem1  44535  xlimmnfv  44537  xlimpnfvlem1  44539  xlimpnfv  44541  cncfshiftioo  44595  fperdvper  44622  itgiccshift  44683  itgperiod  44684  stoweidlem27  44730  stoweidlem31  44734  stoweidlem43  44746  stoweidlem46  44749  stoweidlem52  44755  stoweidlem60  44763  fourierdlem42  44852  fourierdlem48  44857  fourierdlem51  44860  fourierdlem54  44863  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem68  44877  fourierdlem70  44879  fourierdlem71  44880  fourierdlem73  44882  fourierdlem80  44889  fourierdlem81  44890  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem92  44901  fourierdlem96  44905  fourierdlem97  44906  fourierdlem98  44907  fourierdlem99  44908  fourierdlem100  44909  fourierdlem103  44912  fourierdlem104  44913  fourierdlem105  44914  fourierdlem108  44917  fourierdlem109  44918  fourierdlem110  44919  fourierdlem112  44921  fourierdlem113  44922  sge0pnffigt  45099  sge0resplit  45109  ovnval2  45248  ovnval2b  45255  ovnlecvr  45261  ovnpnfelsup  45262  ovn0lem  45268  ovnsubaddlem1  45273  hoidmvlelem1  45298  ovnhoilem1  45304  ovnhoi  45306  ovnlecvr2  45313  hoiqssbl  45328  ovolval5lem2  45356  ovolval5lem3  45357  ovolval5  45358  ovnovol  45362  smfsuplem2  45515  smfsup  45517  smfinflem  45520  smfinf  45521  fsetsnf  45748  fsetsnfo  45750  cfsetsnfsetf  45755  cfsetsnfsetfo  45757  cbvrex2  45799  2reu8i  45808  2reuimp0  45809  afvelrnb  45858  afvelrnb0  45859  elsetpreimafvb  46039  imasetpreimafvbijlemfo  46060  iccelpart  46088  iccpartiun  46089  icceuelpart  46091  sprsymrelf1lem  46146  sprsymrelf  46150  fmtnofac2lem  46223  fmtnofac2  46224  fmtnofac1  46225  m1expevenALTV  46302  odd2np1ALTV  46329  opoeALTV  46338  opeoALTV  46339  mogoldbblem  46375  nfermltlrev  46399  isgbow  46407  isgbo  46408  7gbow  46427  9gbo  46429  11gbo  46430  sbgoldbwt  46432  mogoldbb  46440  sbgoldbo  46442  nnsum3primesgbe  46447  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  bgoldbtbnd  46464  uspgrsprf1  46512  uspgrsprfo  46513  0nodd  46567  1odd  46568  2nodd  46569  0even  46783  1neven  46784  2even  46785  2zlidl  46786  2zrngamgm  46791  2zrngagrp  46795  2zrngmmgm  46798  2zrngnmrid  46802  lcoval  47047  el0ldep  47101  ldepspr  47108  zlmodzxzldep  47139  line  47372  rrxline  47374  sepnsepo  47510