Theorem rexbidv 3225

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
rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rexbidva 3224	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2108  ∃wrex 3064

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-ex 1784  df-rex 3069

This theorem is referenced by:  2rexbidv  3228  rexralbidv  3229  cbvrex2vw  3386  cbvrex2v  3389  rspc2ev  3564  rspc3ev  3566  ceqsrex2v  3580  reuxfr1d  3680  uniiunlem  4015  n0snor2el  4761  eliun  4925  dfiin2g  4958  dfiunv2  4961  dmopab2rex  5815  elrnmpt  5854  elrnmptg  5857  elimag  5962  fvelrnb  6812  fvelimab  6823  foelrn  6964  foco2  6965  elabrex  7098  abrexco  7099  f1oiso  7202  f1oiso2  7203  orduninsuc  7665  funcnvuni  7752  fiunlem  7758  fiun  7759  f1iun  7760  abrexex2g  7780  f1oweALT  7788  el2xptp  7850  tfrlem12  8191  seqomlem2  8252  nneob  8446  qseq2  8511  elqsg  8515  elqsecl  8518  elixpsn  8683  ixpsnf1o  8684  isfi  8719  pssnn  8913  enfiALT  8934  pssnnOLD  8969  frfi  8989  unblem1  8996  unblem2  8997  unbnn2  9001  fofinf1o  9024  finsschain  9056  indexfi  9057  elfi  9102  marypha1lem  9122  supeq3  9138  supmo  9141  suplub  9149  supisolem  9162  eqinf  9173  infval  9175  infglb  9179  infglbb  9180  infmo  9184  oieq1  9201  ordtypelem2  9208  ordtypelem3  9209  ordtypelem9  9215  wemaplem1  9235  brwdom2  9262  brwdom3  9271  unwdomg  9273  oemapval  9371  cantnf  9381  wemapwe  9385  cnfcom3clem  9393  tz9.13  9480  tz9.13g  9481  cardf2  9632  isnum2  9634  ennum  9636  cardiun  9671  infxpenc2  9709  aceq1  9804  aceq2  9806  dfac5lem3  9812  dfac5lem4  9813  dfac2a  9816  dfac2b  9817  kmlem9  9845  kmlem12  9848  kmlem14  9850  ackbij1  9925  cflm  9937  cfss  9952  cofsmo  9956  cfsmolem  9957  cfcoflem  9959  coftr  9960  isfin7  9988  fin23lem26  10012  isf32lem5  10044  fin1a2lem11  10097  hsmexlem2  10114  axdc3lem3  10139  axdc3  10141  numthcor  10181  zorn2lem7  10189  brdom3  10215  brdom7disj  10218  brdom6disj  10219  iundom2g  10227  fpwwe2  10330  winainflem  10380  winalim2  10383  inar1  10462  tskuni  10470  nqereu  10616  prnmax  10682  genpv  10686  genpnmax  10694  genpass  10696  prlem936  10734  recexsrlem  10790  map2psrpr  10797  supsrlem  10798  axrrecex  10850  axpre-sup  10856  dedekind  11068  cnegex  11086  recex  11537  fimaxre3  11851  infm3  11864  supaddc  11872  supadd  11873  supmul1  11874  supmullem1  11875  supmullem2  11876  supmul  11877  creur  11897  creui  11898  cju  11899  nnunb  12159  arch  12160  xrsupsslem  12970  xrinfmsslem  12971  xrsupss  12972  xrinfmss  12973  xrub  12975  supxrunb1  12982  supxrunb2  12983  infmremnf  13006  infmrp1  13007  modmuladd  13561  fsequb2  13624  hashge2el2difr  14123  iswrd  14147  wrdval  14148  csbwrdg  14175  cshword  14432  0csh0  14434  2cshwcshw  14466  scshwfzeqfzo  14467  cshimadifsn  14470  shftfval  14709  abs1m  14975  rexfiuz  14987  reusq0  15102  limsupbnd2  15120  clim  15131  rlim  15132  rlim2  15133  rlim0  15145  rlim0lt  15146  ello1mpt2  15159  o1lo1  15174  o1compt  15224  rlimdiv  15285  climsup  15309  sumeq1  15328  sumeq2w  15332  summo  15357  fsum  15360  fsumcvg3  15369  infcvgaux2i  15498  mertenslem1  15524  mertenslem2  15525  mertens  15526  prodeq1f  15546  prodeq2w  15550  prodmo  15574  fprod  15579  divides  15893  odd2np1lem  15977  opeo  16002  omeo  16003  divalglem4  16033  divalglem10  16039  divalg  16040  gcdcllem3  16136  zeqzmulgcd  16145  bezoutlem1  16175  exprmfct  16337  nnnn0modprm0  16435  pythagtriplem2  16446  pythagtrip  16463  pceu  16475  pcprmpw2  16511  unbenlem  16537  4sqlem12  16585  vdwapval  16602  vdwapun  16603  vdwmc2  16608  vdwpc  16609  vdwlem2  16611  vdwlem10  16619  vdwlem13  16622  vdwnnlem1  16624  rami  16644  cshwsiun  16729  cshwrepswhash1  16732  brssc  17443  cat1  17728  isdrs  17934  drsdir  17935  drsdirfi  17938  isdrs2  17939  ipodrsima  18174  grprinvlem  18272  gsumvalx  18275  gsumpropd  18277  gsumress  18281  isnsgrp  18294  smndex2dnrinv  18469  sgrp2nmndlem5  18483  grpinvex  18502  dfgrp2  18519  grpidinv2  18549  grpidinv  18550  dfgrp3lem  18588  grp1  18597  imasgrp2  18605  cyccom  18737  conjnmzb  18784  gaorb  18828  orbsta  18834  symgfix2  18939  symgextfo  18945  pmtrprfvalrn  19011  psgnunilem3  19019  psgneu  19029  psgnval  19030  psgnvali  19031  psgnvalii  19032  ispgp  19112  subgpgp  19117  sylow1  19123  pgpfi  19125  sylow2blem3  19142  fislw  19145  sylow3lem2  19148  lsmelvalm  19171  lsmass  19190  pj1fval  19215  pj1val  19216  pj1eu  19217  pj1id  19220  efgrelexlema  19270  efgrelexlemb  19271  efgredeu  19273  cyggeninv  19398  cygablOLD  19407  pgpfac1lem2  19593  pgpfac1lem3  19595  pgpfac1lem4  19596  pgpfac1  19598  pgpfaclem2  19600  pgpfac  19602  dvdsrval  19802  dvdsr  19803  subrgdvds  19953  lss1d  20140  lspsn  20179  lspsnel  20180  lspsolvlem  20319  rspsn  20438  znf1o  20671  cygznlem3  20689  psgndiflemA  20718  ellspd  20919  opsrval  21157  mat1dimelbas  21528  mat1dimbas  21529  scmatval  21561  scmatel  21562  scmateALT  21569  mat0scmat  21595  decpmataa0  21825  decpmatmulsumfsupp  21830  pmatcollpw2lem  21834  pm2mpmhmlem1  21875  chpscmat  21899  basis2  22009  eltg2  22016  tg2  22023  isclo  22146  neival  22161  isnei  22162  isneip  22164  restbas  22217  neitr  22239  cnpval  22295  iscnp  22296  cnpimaex  22315  lmbr  22317  lmbr2  22318  cnprest2  22349  lmff  22360  regsep  22393  pnrmopn  22402  nrmsep3  22414  isnrm2  22417  iscmp  22447  cmpsublem  22458  cmpsub  22459  tgcmp  22460  sscmp  22464  hauscmplem  22465  1stcclb  22503  1stcfb  22504  is2ndc  22505  2ndc1stc  22510  1stcrest  22512  2ndcctbss  22514  1stcelcls  22520  llyeq  22529  nllyeq  22530  hausllycmp  22553  lly1stc  22555  refssex  22570  refun0  22574  islocfin  22576  locfinnei  22582  comppfsc  22591  txbas  22626  ptval  22629  ptpjopn  22671  ptclsg  22674  txcnp  22679  ptcnp  22681  txrest  22690  ptrescn  22698  txcmp  22702  tx1stc  22709  xkococn  22719  kqreglem1  22800  fbasssin  22895  fbssfi  22896  fbssint  22897  fbun  22899  fgss2  22933  fgcl  22937  ufli  22973  fmfnfmlem3  23015  fbflim2  23036  hauspwpwf1  23046  flfneii  23051  flftg  23055  txflf  23065  fclscf  23084  alexsubb  23105  alexsubALT  23110  tsmssubm  23202  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ust0  23279  trust  23289  elutop  23293  ucnval  23337  ucncn  23345  cfiluexsm  23350  cfiluweak  23355  blssps  23485  blss  23486  imasf1oxms  23551  mopni  23554  metss  23570  metrest  23586  metcnp3  23602  cfilucfil  23621  metuel2  23627  nlmvscn  23757  nrginvrcn  23762  icccmplem1  23891  icccmplem2  23892  icccmp  23894  divcn  23937  cncfval  23957  elcncf2  23959  cncfmet  23978  cnheibor  24024  evth  24028  lebnumlem3  24032  lebnum  24033  xlebnum  24034  lebnumii  24035  ipcn  24315  lmmbr  24327  lmmbr2  24328  cfilfval  24333  cfili  24337  iscfil3  24342  caufval  24344  iscau  24345  iscau2  24346  equivcfil  24368  equivcau  24369  lmcau  24382  ovolval  24542  elovolm  24544  ovolgelb  24549  ovoliunlem1  24571  ovoliun2  24575  ovolshftlem1  24578  ovolscalem1  24582  ovolicc  24592  ioombl1lem4  24630  uniioombllem2  24652  mbfaddlem  24729  mbfsup  24733  mbfinf  24734  mbflimsup  24735  i1fmulc  24773  itg1climres  24784  itg2val  24798  itg2l  24799  itg2leub  24804  itg2seq  24812  itg2monolem1  24820  itg2mono  24823  itg2i1fseq2  24826  cniccibl  24910  cnicciblnc  24912  ellimc3  24948  limciun  24963  dvferm1  25054  dvferm2  25056  lhop1lem  25082  ply1divex  25206  ig1peu  25241  plyval  25259  elply2  25262  coeval  25289  coeeu  25291  coelem  25292  coeeq  25293  plydivlem4  25361  plydivex  25362  aannenlem2  25394  aalioulem2  25398  aaliou2  25405  ulmval  25444  ulm2  25449  ulmcau  25459  ulmdvlem3  25466  abelthlem9  25504  abelth  25505  efif1olem4  25606  eflogeq  25662  efopn  25718  cxpcn3  25806  cxpeq  25815  rlimcnp  26020  lgamgulmlem6  26088  muval  26186  dchrptlem1  26317  dchrptlem2  26318  lgsdchrval  26407  2lgslem1b  26445  addsq2nreurex  26497  pntpbnd  26641  pntibndlem3  26645  pntibnd  26646  pntlemi  26657  pntleme  26661  pntlemp  26663  pnt3  26665  istrkgld  26724  istrkg3ld  26726  axtgsegcon  26729  axtgpasch  26732  axtgcont1  26733  axtgupdim2  26736  legov  26850  islnopp  27004  ishpg  27024  hpgbr  27025  hpgcom  27032  iscgra1  27075  isinag  27103  isleag  27112  ttgval  27140  ttgitvval  27152  ttgelitv  27153  brbtwn  27170  brcgr  27171  axpasch  27212  axlowdim2  27231  axlowdim  27232  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  upgredg2vtx  27414  edglnl  27416  usgredg4  27487  ushgredgedg  27499  ushgredgedgloop  27501  dfnbgr2  27607  nbgrel  27610  nbumgrvtx  27616  nbgrnself  27629  uvtxel1  27666  cusgrfilem2  27726  cusgrfi  27728  vtxd0nedgb  27758  fusgrn0degnn0  27769  wlkonl1iedg  27935  wspniunwspnon  28189  elwwlks2on  28225  clwwlknscsh  28327  erclwwlkneq  28332  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  3cyclfrgrrn1  28550  friendshipgt3  28663  isgrpo  28760  isgrpoi  28761  grpoidinvlem3  28769  grpoideu  28772  grpoidinv2  28778  nmoofval  29025  nmooval  29026  nmosetn0  29028  nmoolb  29034  nmoubi  29035  nmlno0lem  29056  chcompl  29505  pjhthmo  29565  pjhval  29660  pjpreeq  29661  h1de2ci  29819  elspansn  29829  nmopval  30119  nmopsetn0  30128  nmfnval  30139  nmfnsetn0  30141  eigvecval  30159  hhcno  30167  hhcnf  30168  nmoplb  30170  nmopub  30171  nmfnlb  30187  nmfnleub  30188  eleigvec  30220  nmlnop0iALT  30258  nmopun  30277  nmcexi  30289  branmfn  30368  pjnmopi  30411  cvbr  30545  hatomic  30623  chrelat2  30633  cdjreui  30695  cdj3lem2  30698  elabreximd  30756  br8d  30851  unipreima  30882  abfmpunirn  30891  curry2ima  30943  toslublem  31152  tosglblem  31154  cyc3genpm  31321  archirng  31344  archiexdiv  31346  archiabllem2a  31350  archiabl  31354  isarchiofld  31418  elgrplsmsn  31480  lsmssass  31492  grplsm0l  31493  grplsmid  31494  mxidlprm  31542  fedgmul  31614  ccfldextdgrr  31644  crefi  31699  pcmplfin  31712  rspectopn  31719  pstmfval  31748  tpr2rico  31764  rge0scvg  31801  ismntop  31876  esumc  31919  esumpcvgval  31946  esum2dlem  31960  inelsros  32046  diffiunisros  32047  dya2icoseg2  32145  dya2iocuni  32150  eulerpartlemgvv  32243  eulerpartlemgh  32245  hgt749d  32529  tgoldbachgt  32543  bnj66  32740  bnj873  32804  bnj18eq1  32807  bnj1234  32893  bnj1318  32905  cplgredgex  32982  subfacp1lem3  33044  pconncn  33086  cnpconn  33092  txpconn  33094  connpconn  33097  iscvm  33121  cvmcov  33125  cvmopnlem  33140  cvmliftlem15  33160  cvmlift3lem2  33182  cvmlift3lem4  33184  cvmlift3  33190  satf  33215  satfv1  33225  satfvsucsuc  33227  satfbrsuc  33228  satfrnmapom  33232  satf0op  33239  sat1el2xp  33241  fmlafvel  33247  fmlasuc  33248  fmla1  33249  isfmlasuc  33250  fmlaomn0  33252  fmlasucdisj  33261  satffunlem1lem1  33264  satffunlem1lem2  33265  satffunlem2lem1  33266  dmopab3rexdif  33267  satffunlem2lem2  33268  sategoelfvb  33281  satfv1fvfmla1  33285  2goelgoanfmla1  33286  elxpxp  33586  eldifsucnn  33597  br8  33629  br6  33630  br4  33631  dfrdg2  33677  dfrdg3  33678  ttrcleq  33695  brttrcl  33699  ttrcltr  33702  orderseqlem  33728  poseq  33729  soseq  33730  elno  33776  sltval  33777  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupno  33833  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  noinfcbv  33847  noinfno  33848  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  madef  33967  cofsslt  34015  coinitsslt  34016  addsval  34053  addscllem1  34058  altxpeq2  34203  funtransport  34260  fvtransport  34261  brcolinear2  34287  colineardim1  34290  segcon2  34334  brsegle  34337  funray  34369  fvray  34370  funline  34371  linedegen  34372  fvline  34373  ellines  34381  nn0prpwlem  34438  fnessref  34473  neibastop2lem  34476  neibastop2  34477  tailfb  34493  unblimceq0lem  34613  unblimceq0  34614  unbdqndv2  34618  bj-finsumval0  35383  relowlssretop  35461  nlpineqsn  35506  pibp19  35512  phpreu  35688  matunitlindflem2  35701  ptrest  35703  poimirlem4  35708  poimirlem17  35721  poimirlem20  35724  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem31  35735  poimirlem32  35736  poimir  35737  heicant  35739  mblfinlem1  35741  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ftc1anclem6  35782  unirep  35798  indexa  35818  sdclem2  35827  sdclem1  35828  sdc  35829  fdc  35830  fdc1  35831  incsequz  35833  istotbnd  35854  sstotbnd2  35859  equivtotbnd  35863  isbnd  35865  bndss  35871  ssbnd  35873  totbndbnd  35874  ismtybndlem  35891  heibor1lem  35894  heiborlem1  35896  heiborlem6  35901  heiborlem8  35903  heiborlem10  35905  heibor  35906  rngoid  35987  isgrpda  36040  isdrngo2  36043  divrngidl  36113  prnc  36152  isfldidl  36153  exanres3  36358  brcoels  36485  br1cossxrnres  36493  eldm1cossres2  36506  prtlem5  36801  prtlem13  36809  prtlem16  36810  islshp  36920  lsmsat  36949  lcvbr  36962  lsatcv0  36972  lshpsmreu  37050  lshpkrlem1  37051  lshpkrlem2  37052  lshpkrlem3  37053  lshpkrcl  37057  lshpset2N  37060  islshpkrN  37061  cvrval  37210  atlex  37257  glbconxN  37319  hlsuprexch  37322  islln  37447  islpln  37471  islpln5  37476  lvolex3N  37479  islvol  37514  islvol5  37520  ispointN  37683  pmapglbx  37710  paddval  37739  elpaddn0  37741  elpaddat  37745  elpadd0  37750  4atex  38017  4atex2  38018  cdlemefrs29bpre1  38338  cdlemefrs32fva  38341  cdlemg33b  38648  dvhb1dimN  38927  dvhopellsm  39058  dib1dim  39106  diclspsn  39135  dihglblem2aN  39234  dihglblem2N  39235  dih1dimatlem  39270  dvh3dimatN  39380  dvh2dim  39386  dvh3dim  39387  dvh4dimN  39388  dvh3dim3N  39390  dochfl1  39417  lcfl7N  39442  lcf1o  39492  lcfrlem39  39522  mapdpglem3  39616  hvmapvalvalN  39702  hdmap14lem2a  39808  hdmapglem7a  39868  3factsumint1  39957  3rspcedvd  40110  nnn1suc  40217  prjspeclsp  40372  elrfi  40432  isnacs  40442  nacsfg  40443  nacsfix  40450  mzpcompact2lem  40489  eldiophb  40495  eldioph  40496  eldioph2  40500  eldioph2b  40501  eldioph3  40504  eldiophss  40512  diophrex  40513  sbcrexgOLD  40523  sbc2rexgOLD  40526  rexrabdioph  40532  rexfrabdioph  40533  elnn0rabdioph  40541  dvdsrabdioph  40548  eldioph4b  40549  eldioph4i  40550  diophren  40551  rencldnfilem  40558  pell1234qrdich  40599  jm2.27  40746  expdiophlem1  40759  wepwsolem  40783  aomclem8  40802  islnr3  40856  lnr2i  40857  lpirlnr  40858  hbtlem1  40864  hbtlem2  40865  hbtlem7  40866  hbtlem4  40867  hbtlem5  40869  hbtlem6  40870  dgraaval  40885  dgraalem  40886  dgraaub  40889  rngunsnply  40914  brtrclfv2  41224  clsk1indlem1  41544  extoimad  41664  mnuop123d  41769  mnuop23d  41773  mnuprdlem1  41779  mnuprdlem2  41780  ismnushort  41808  elabrexg  42478  foelrnf  42613  disjrnmpt2  42615  upbdrech  42734  ssfiunibd  42738  supxrgere  42762  supxrgelem  42766  supxrge  42767  suplesup  42768  infxr  42796  infleinf  42801  supxrunb3  42829  unb2ltle  42845  uzub  42861  supminfxr  42894  iccshift  42946  iooshift  42950  climinf  43037  climinff  43042  ellimcabssub0  43048  climf  43053  limcperiod  43059  limclner  43082  climf2  43097  clim2d  43104  limsuppnfd  43133  limsuppnf  43142  climinfmpt  43146  limsupubuzmpt  43150  limsupmnf  43152  limsupre2lem  43155  limsupre2  43156  limsupmnfuz  43158  limsupre2mpt  43161  limsupre3lem  43163  limsupre3  43164  limsupre3mpt  43165  limsupre3uzlem  43166  limsupre3uz  43167  limsupreuz  43168  limsupreuzmpt  43170  climuz  43175  liminfreuzlem  43233  liminfreuz  43234  xlimmnfvlem1  43263  xlimmnfv  43265  xlimpnfvlem1  43267  xlimpnfv  43269  cncfshiftioo  43323  fperdvper  43350  itgiccshift  43411  itgperiod  43412  stoweidlem27  43458  stoweidlem31  43462  stoweidlem43  43474  stoweidlem46  43477  stoweidlem52  43483  stoweidlem60  43491  fourierdlem42  43580  fourierdlem48  43585  fourierdlem51  43588  fourierdlem54  43591  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem68  43605  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem80  43617  fourierdlem81  43618  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem100  43637  fourierdlem103  43640  fourierdlem104  43641  fourierdlem105  43642  fourierdlem108  43645  fourierdlem109  43646  fourierdlem110  43647  fourierdlem112  43649  fourierdlem113  43650  sge0pnffigt  43824  sge0resplit  43834  ovnval2  43973  ovnval2b  43980  ovnlecvr  43986  ovnpnfelsup  43987  ovn0lem  43993  ovnsubaddlem1  43998  hoidmvlelem1  44023  ovnhoilem1  44029  ovnhoi  44031  ovnlecvr2  44038  hoiqssbl  44053  ovolval5lem2  44081  ovolval5lem3  44082  ovolval5  44083  ovnovol  44087  smfsuplem2  44232  smfsup  44234  smfinflem  44237  smfinf  44238  fsetsnf  44432  fsetsnfo  44434  cfsetsnfsetf  44439  cfsetsnfsetfo  44441  cbvrex2  44483  2reu8i  44492  2reuimp0  44493  afvelrnb  44542  afvelrnb0  44543  elsetpreimafvb  44724  imasetpreimafvbijlemfo  44745  iccelpart  44773  iccpartiun  44774  icceuelpart  44776  sprsymrelf1lem  44831  sprsymrelf  44835  fmtnofac2lem  44908  fmtnofac2  44909  fmtnofac1  44910  m1expevenALTV  44987  odd2np1ALTV  45014  opoeALTV  45023  opeoALTV  45024  mogoldbblem  45060  nfermltlrev  45084  isgbow  45092  isgbo  45093  7gbow  45112  9gbo  45114  11gbo  45115  sbgoldbwt  45117  mogoldbb  45125  sbgoldbo  45127  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  bgoldbtbnd  45149  uspgrsprf1  45197  uspgrsprfo  45198  0nodd  45252  1odd  45253  2nodd  45254  0even  45377  1neven  45378  2even  45379  2zlidl  45380  2zrngamgm  45385  2zrngagrp  45389  2zrngmmgm  45392  2zrngnmrid  45396  lcoval  45641  el0ldep  45695  ldepspr  45702  zlmodzxzldep  45733  line  45966  rrxline  45968  sepnsepo  46105