Theorem rexbidv 3256

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 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rexbidva 3255	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111  ∃wrex 3107

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  2rexbidv  3259  rexralbidv  3260  cbvrex2vw  3409  cbvrex2v  3412  rspc2ev  3583  rspc3ev  3585  ceqsrex2v  3599  reuxfr1d  3689  uniiunlem  4012  n0snor2el  4724  eliun  4885  dfiin2g  4919  dfiunv2  4922  dmopab2rex  5750  elrnmpt  5792  elrnmptg  5795  elimag  5900  fvelrnb  6701  fvelimab  6712  foelrn  6849  foco2  6850  elabrex  6980  abrexco  6981  f1oiso  7083  f1oiso2  7084  orduninsuc  7538  funcnvuni  7618  fiunlem  7625  fiun  7626  f1iun  7627  abrexex2g  7647  f1oweALT  7655  el2xptp  7717  tfrlem12  8008  seqomlem2  8070  nneob  8262  qseq2  8327  elqsg  8331  elqsecl  8334  elixpsn  8484  ixpsnf1o  8485  isfi  8516  enfi  8718  pssnn  8720  frfi  8747  unblem1  8754  unblem2  8755  unbnn2  8759  fofinf1o  8783  finsschain  8815  indexfi  8816  elfi  8861  marypha1lem  8881  supeq3  8897  supmo  8900  suplub  8908  supisolem  8921  eqinf  8932  infval  8934  infglb  8938  infglbb  8939  infmo  8943  oieq1  8960  ordtypelem2  8967  ordtypelem3  8968  ordtypelem9  8974  wemaplem1  8994  brwdom2  9021  brwdom3  9030  unwdomg  9032  oemapval  9130  cantnf  9140  wemapwe  9144  cnfcom3clem  9152  tz9.13  9204  tz9.13g  9205  cardf2  9356  isnum2  9358  ennum  9360  cardiun  9395  infxpenc2  9433  aceq1  9528  aceq2  9530  dfac5lem3  9536  dfac5lem4  9537  dfac2a  9540  dfac2b  9541  kmlem9  9569  kmlem12  9572  kmlem14  9574  ackbij1  9649  cflm  9661  cfss  9676  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  coftr  9684  isfin7  9712  fin23lem26  9736  isf32lem5  9768  fin1a2lem11  9821  hsmexlem2  9838  axdc3lem3  9863  axdc3  9865  numthcor  9905  zorn2lem7  9913  brdom3  9939  brdom7disj  9942  brdom6disj  9943  iundom2g  9951  fpwwe2  10054  winainflem  10104  winalim2  10107  inar1  10186  tskuni  10194  nqereu  10340  prnmax  10406  genpv  10410  genpnmax  10418  genpass  10420  prlem936  10458  recexsrlem  10514  map2psrpr  10521  supsrlem  10522  axrrecex  10574  axpre-sup  10580  dedekind  10792  cnegex  10810  recex  11261  fimaxre3  11575  infm3  11587  supaddc  11595  supadd  11596  supmul1  11597  supmullem1  11598  supmullem2  11599  supmul  11600  creur  11619  creui  11620  cju  11621  nnunb  11881  arch  11882  xrsupsslem  12688  xrinfmsslem  12689  xrsupss  12690  xrinfmss  12691  xrub  12693  supxrunb1  12700  supxrunb2  12701  infmremnf  12724  infmrp1  12725  modmuladd  13276  fsequb2  13339  hashge2el2difr  13835  iswrd  13859  wrdval  13860  csbwrdg  13887  cshword  14144  0csh0  14146  2cshwcshw  14178  scshwfzeqfzo  14179  cshimadifsn  14182  shftfval  14421  abs1m  14687  rexfiuz  14699  reusq0  14814  limsupbnd2  14832  clim  14843  rlim  14844  rlim2  14845  rlim0  14857  rlim0lt  14858  ello1mpt2  14871  o1lo1  14886  o1compt  14936  rlimdiv  14994  climsup  15018  sumeq1  15037  sumeq2w  15041  summo  15066  fsum  15069  fsumcvg3  15078  infcvgaux2i  15205  mertenslem1  15232  mertenslem2  15233  mertens  15234  prodeq1f  15254  prodeq2w  15258  prodmo  15282  fprod  15287  divides  15601  odd2np1lem  15681  opeo  15706  omeo  15707  divalglem4  15737  divalglem10  15743  divalg  15744  gcdcllem3  15840  zeqzmulgcd  15849  bezoutlem1  15877  exprmfct  16038  nnnn0modprm0  16133  pythagtriplem2  16144  pythagtrip  16161  pceu  16173  pcprmpw2  16208  unbenlem  16234  4sqlem12  16282  vdwapval  16299  vdwapun  16300  vdwmc2  16305  vdwpc  16306  vdwlem2  16308  vdwlem10  16316  vdwlem13  16319  vdwnnlem1  16321  rami  16341  cshwsiun  16425  cshwrepswhash1  16428  brssc  17076  isdrs  17536  drsdir  17537  drsdirfi  17540  isdrs2  17541  ipodrsima  17767  grprinvlem  17875  gsumvalx  17878  gsumpropd  17880  gsumress  17884  isnsgrp  17897  smndex2dnrinv  18072  sgrp2nmndlem5  18086  grpinvex  18105  dfgrp2  18120  grpidinv2  18150  grpidinv  18151  dfgrp3lem  18189  grp1  18198  imasgrp2  18206  cyccom  18338  conjnmzb  18385  gaorb  18429  orbsta  18435  symgfix2  18536  symgextfo  18542  pmtrprfvalrn  18608  psgnunilem3  18616  psgneu  18626  psgnval  18627  psgnvali  18628  psgnvalii  18629  ispgp  18709  subgpgp  18714  sylow1  18720  pgpfi  18722  sylow2blem3  18739  fislw  18742  sylow3lem2  18745  lsmelvalm  18768  lsmass  18787  pj1fval  18812  pj1val  18813  pj1eu  18814  pj1id  18817  efgrelexlema  18867  efgrelexlemb  18868  efgredeu  18870  cyggeninv  18995  cygablOLD  19004  pgpfac1lem2  19190  pgpfac1lem3  19192  pgpfac1lem4  19193  pgpfac1  19195  pgpfaclem2  19197  pgpfac  19199  dvdsrval  19391  dvdsr  19392  subrgdvds  19542  lss1d  19728  lspsn  19767  lspsnel  19768  lspsolvlem  19907  rspsn  20020  znf1o  20243  cygznlem3  20261  psgndiflemA  20290  ellspd  20491  opsrval  20714  mat1dimelbas  21076  mat1dimbas  21077  scmatval  21109  scmatel  21110  scmateALT  21117  mat0scmat  21143  decpmataa0  21373  decpmatmulsumfsupp  21378  pmatcollpw2lem  21382  pm2mpmhmlem1  21423  chpscmat  21447  basis2  21556  eltg2  21563  tg2  21570  isclo  21692  neival  21707  isnei  21708  isneip  21710  restbas  21763  neitr  21785  cnpval  21841  iscnp  21842  cnpimaex  21861  lmbr  21863  lmbr2  21864  cnprest2  21895  lmff  21906  regsep  21939  pnrmopn  21948  nrmsep3  21960  isnrm2  21963  iscmp  21993  cmpsublem  22004  cmpsub  22005  tgcmp  22006  sscmp  22010  hauscmplem  22011  1stcclb  22049  1stcfb  22050  is2ndc  22051  2ndc1stc  22056  1stcrest  22058  2ndcctbss  22060  1stcelcls  22066  llyeq  22075  nllyeq  22076  hausllycmp  22099  lly1stc  22101  refssex  22116  refun0  22120  islocfin  22122  locfinnei  22128  comppfsc  22137  txbas  22172  ptval  22175  ptpjopn  22217  ptclsg  22220  txcnp  22225  ptcnp  22227  txrest  22236  ptrescn  22244  txcmp  22248  tx1stc  22255  xkococn  22265  kqreglem1  22346  fbasssin  22441  fbssfi  22442  fbssint  22443  fbun  22445  fgss2  22479  fgcl  22483  ufli  22519  fmfnfmlem3  22561  fbflim2  22582  hauspwpwf1  22592  flfneii  22597  flftg  22601  txflf  22611  fclscf  22630  alexsubb  22651  alexsubALT  22656  tsmssubm  22748  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  ust0  22825  trust  22835  elutop  22839  ucnval  22883  ucncn  22891  cfiluexsm  22896  cfiluweak  22901  blssps  23031  blss  23032  imasf1oxms  23096  mopni  23099  metss  23115  metrest  23131  metcnp3  23147  cfilucfil  23166  metuel2  23172  nlmvscn  23293  nrginvrcn  23298  icccmplem1  23427  icccmplem2  23428  icccmp  23430  divcn  23473  cncfval  23493  elcncf2  23495  cncfmet  23514  cnheibor  23560  evth  23564  lebnumlem3  23568  lebnum  23569  xlebnum  23570  lebnumii  23571  ipcn  23850  lmmbr  23862  lmmbr2  23863  cfilfval  23868  cfili  23872  iscfil3  23877  caufval  23879  iscau  23880  iscau2  23881  equivcfil  23903  equivcau  23904  lmcau  23917  ovolval  24077  elovolm  24079  ovolgelb  24084  ovoliunlem1  24106  ovoliun2  24110  ovolshftlem1  24113  ovolscalem1  24117  ovolicc  24127  ioombl1lem4  24165  uniioombllem2  24187  mbfaddlem  24264  mbfsup  24268  mbfinf  24269  mbflimsup  24270  i1fmulc  24307  itg1climres  24318  itg2val  24332  itg2l  24333  itg2leub  24338  itg2seq  24346  itg2monolem1  24354  itg2mono  24357  itg2i1fseq2  24360  cniccibl  24444  cnicciblnc  24446  ellimc3  24482  limciun  24497  dvferm1  24588  dvferm2  24590  lhop1lem  24616  ply1divex  24737  ig1peu  24772  plyval  24790  elply2  24793  coeval  24820  coeeu  24822  coelem  24823  coeeq  24824  plydivlem4  24892  plydivex  24893  aannenlem2  24925  aalioulem2  24929  aaliou2  24936  ulmval  24975  ulm2  24980  ulmcau  24990  ulmdvlem3  24997  abelthlem9  25035  abelth  25036  efif1olem4  25137  eflogeq  25193  efopn  25249  cxpcn3  25337  cxpeq  25346  rlimcnp  25551  lgamgulmlem6  25619  muval  25717  dchrptlem1  25848  dchrptlem2  25849  lgsdchrval  25938  2lgslem1b  25976  addsq2nreurex  26028  pntpbnd  26172  pntibndlem3  26176  pntibnd  26177  pntlemi  26188  pntleme  26192  pntlemp  26194  pnt3  26196  istrkgld  26253  istrkg3ld  26255  axtgsegcon  26258  axtgpasch  26261  axtgcont1  26262  axtgupdim2  26265  legov  26379  islnopp  26533  ishpg  26553  hpgbr  26554  hpgcom  26561  iscgra1  26604  isinag  26632  isleag  26641  ttgval  26669  ttgitvval  26676  ttgelitv  26677  brbtwn  26693  brcgr  26694  axpasch  26735  axlowdim2  26754  axlowdim  26755  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  upgredg2vtx  26934  edglnl  26936  usgredg4  27007  ushgredgedg  27019  ushgredgedgloop  27021  dfnbgr2  27127  nbgrel  27130  nbumgrvtx  27136  nbgrnself  27149  uvtxel1  27186  cusgrfilem2  27246  cusgrfi  27248  vtxd0nedgb  27278  fusgrn0degnn0  27289  wlkonl1iedg  27455  wspniunwspnon  27709  elwwlks2on  27745  clwwlknscsh  27847  erclwwlkneq  27852  eleclclwwlkn  27861  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  3cyclfrgrrn1  28070  friendshipgt3  28183  isgrpo  28280  isgrpoi  28281  grpoidinvlem3  28289  grpoideu  28292  grpoidinv2  28298  nmoofval  28545  nmooval  28546  nmosetn0  28548  nmoolb  28554  nmoubi  28555  nmlno0lem  28576  chcompl  29025  pjhthmo  29085  pjhval  29180  pjpreeq  29181  h1de2ci  29339  elspansn  29349  nmopval  29639  nmopsetn0  29648  nmfnval  29659  nmfnsetn0  29661  eigvecval  29679  hhcno  29687  hhcnf  29688  nmoplb  29690  nmopub  29691  nmfnlb  29707  nmfnleub  29708  eleigvec  29740  nmlnop0iALT  29778  nmopun  29797  nmcexi  29809  branmfn  29888  pjnmopi  29931  cvbr  30065  hatomic  30143  chrelat2  30153  cdjreui  30215  cdj3lem2  30218  elabreximd  30278  br8d  30374  unipreima  30405  abfmpunirn  30415  curry2ima  30468  toslublem  30680  tosglblem  30682  cyc3genpm  30844  archirng  30867  archiexdiv  30869  archiabllem2a  30873  archiabl  30877  isarchiofld  30941  elgrplsmsn  30998  lsmssass  31009  mxidlprm  31048  fedgmul  31115  ccfldextdgrr  31145  crefi  31200  pcmplfin  31213  rspectopn  31220  pstmfval  31249  tpr2rico  31265  rge0scvg  31302  ismntop  31377  esumc  31420  esumpcvgval  31447  esum2dlem  31461  inelsros  31547  diffiunisros  31548  dya2icoseg2  31646  dya2iocuni  31651  eulerpartlemgvv  31744  eulerpartlemgh  31746  hgt749d  32030  tgoldbachgt  32044  bnj66  32242  bnj873  32306  bnj18eq1  32309  bnj1234  32395  bnj1318  32407  cplgredgex  32480  subfacp1lem3  32542  pconncn  32584  cnpconn  32590  txpconn  32592  connpconn  32595  iscvm  32619  cvmcov  32623  cvmopnlem  32638  cvmliftlem15  32658  cvmlift3lem2  32680  cvmlift3lem4  32682  cvmlift3  32688  satf  32713  satfv1  32723  satfvsucsuc  32725  satfbrsuc  32726  satfrnmapom  32730  satf0op  32737  sat1el2xp  32739  fmlafvel  32745  fmlasuc  32746  fmla1  32747  isfmlasuc  32748  fmlaomn0  32750  fmlasucdisj  32759  satffunlem1lem1  32762  satffunlem1lem2  32763  satffunlem2lem1  32764  dmopab3rexdif  32765  satffunlem2lem2  32766  sategoelfvb  32779  satfv1fvfmla1  32783  2goelgoanfmla1  32784  br8  33105  br6  33106  br4  33107  dfrdg2  33153  dfrdg3  33154  orderseqlem  33207  poseq  33208  soseq  33209  elno  33266  sltval  33267  noprefixmo  33315  nosupno  33316  nosupdm  33317  nosupfv  33319  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  noeta  33335  altxpeq2  33548  funtransport  33605  fvtransport  33606  brcolinear2  33632  colineardim1  33635  segcon2  33679  brsegle  33682  funray  33714  fvray  33715  funline  33716  linedegen  33717  fvline  33718  ellines  33726  nn0prpwlem  33783  fnessref  33818  neibastop2lem  33821  neibastop2  33822  tailfb  33838  unblimceq0lem  33958  unblimceq0  33959  unbdqndv2  33963  bj-finsumval0  34700  relowlssretop  34780  nlpineqsn  34825  pibp19  34831  phpreu  35041  matunitlindflem2  35054  ptrest  35056  poimirlem4  35061  poimirlem17  35074  poimirlem20  35077  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem31  35088  poimirlem32  35089  poimir  35090  heicant  35092  mblfinlem1  35094  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  ftc1anclem6  35135  unirep  35151  indexa  35171  sdclem2  35180  sdclem1  35181  sdc  35182  fdc  35183  fdc1  35184  incsequz  35186  istotbnd  35207  sstotbnd2  35212  equivtotbnd  35216  isbnd  35218  bndss  35224  ssbnd  35226  totbndbnd  35227  ismtybndlem  35244  heibor1lem  35247  heiborlem1  35249  heiborlem6  35254  heiborlem8  35256  heiborlem10  35258  heibor  35259  rngoid  35340  isgrpda  35393  isdrngo2  35396  divrngidl  35466  prnc  35505  isfldidl  35506  exanres3  35713  brcoels  35840  br1cossxrnres  35848  eldm1cossres2  35861  prtlem5  36156  prtlem13  36164  prtlem16  36165  islshp  36275  lsmsat  36304  lcvbr  36317  lsatcv0  36327  lshpsmreu  36405  lshpkrlem1  36406  lshpkrlem2  36407  lshpkrlem3  36408  lshpkrcl  36412  lshpset2N  36415  islshpkrN  36416  cvrval  36565  atlex  36612  glbconxN  36674  hlsuprexch  36677  islln  36802  islpln  36826  islpln5  36831  lvolex3N  36834  islvol  36869  islvol5  36875  ispointN  37038  pmapglbx  37065  paddval  37094  elpaddn0  37096  elpaddat  37100  elpadd0  37105  4atex  37372  4atex2  37373  cdlemefrs29bpre1  37693  cdlemefrs32fva  37696  cdlemg33b  38003  dvhb1dimN  38282  dvhopellsm  38413  dib1dim  38461  diclspsn  38490  dihglblem2aN  38589  dihglblem2N  38590  dih1dimatlem  38625  dvh3dimatN  38735  dvh2dim  38741  dvh3dim  38742  dvh4dimN  38743  dvh3dim3N  38745  dochfl1  38772  lcfl7N  38797  lcf1o  38847  lcfrlem39  38877  mapdpglem3  38971  hvmapvalvalN  39057  hdmap14lem2a  39163  hdmapglem7a  39223  3factsumint1  39309  3rspcedvd  39397  nnn1suc  39467  prjspeclsp  39606  elrfi  39635  isnacs  39645  nacsfg  39646  nacsfix  39653  mzpcompact2lem  39692  eldiophb  39698  eldioph  39699  eldioph2  39703  eldioph2b  39704  eldioph3  39707  eldiophss  39715  diophrex  39716  sbcrexgOLD  39726  sbc2rexgOLD  39729  rexrabdioph  39735  rexfrabdioph  39736  elnn0rabdioph  39744  dvdsrabdioph  39751  eldioph4b  39752  eldioph4i  39753  diophren  39754  rencldnfilem  39761  pell1234qrdich  39802  jm2.27  39949  expdiophlem1  39962  wepwsolem  39986  aomclem8  40005  islnr3  40059  lnr2i  40060  lpirlnr  40061  hbtlem1  40067  hbtlem2  40068  hbtlem7  40069  hbtlem4  40070  hbtlem5  40072  hbtlem6  40073  dgraaval  40088  dgraalem  40089  dgraaub  40092  rngunsnply  40117  brtrclfv2  40428  clsk1indlem1  40748  extoimad  40868  mnuop123d  40970  mnuop23d  40974  mnuprdlem1  40980  mnuprdlem2  40981  elabrexg  41675  foelrnf  41813  disjrnmpt2  41815  upbdrech  41937  ssfiunibd  41941  supxrgere  41965  supxrgelem  41969  supxrge  41970  suplesup  41971  infxr  41999  infleinf  42004  supxrunb3  42036  unb2ltle  42052  uzub  42068  supminfxr  42103  iccshift  42155  iooshift  42159  climinf  42248  climinff  42253  ellimcabssub0  42259  climf  42264  limcperiod  42270  limclner  42293  climf2  42308  clim2d  42315  limsuppnfd  42344  limsuppnf  42353  climinfmpt  42357  limsupubuzmpt  42361  limsupmnf  42363  limsupre2lem  42366  limsupre2  42367  limsupmnfuz  42369  limsupre2mpt  42372  limsupre3lem  42374  limsupre3  42375  limsupre3mpt  42376  limsupre3uzlem  42377  limsupre3uz  42378  limsupreuz  42379  limsupreuzmpt  42381  climuz  42386  liminfreuzlem  42444  liminfreuz  42445  xlimmnfvlem1  42474  xlimmnfv  42476  xlimpnfvlem1  42478  xlimpnfv  42480  cncfshiftioo  42534  fperdvper  42561  itgiccshift  42622  itgperiod  42623  stoweidlem27  42669  stoweidlem31  42673  stoweidlem43  42685  stoweidlem46  42688  stoweidlem52  42694  stoweidlem60  42702  fourierdlem42  42791  fourierdlem48  42796  fourierdlem51  42799  fourierdlem54  42802  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem68  42816  fourierdlem70  42818  fourierdlem71  42819  fourierdlem73  42821  fourierdlem80  42828  fourierdlem81  42829  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem92  42840  fourierdlem96  42844  fourierdlem97  42845  fourierdlem98  42846  fourierdlem99  42847  fourierdlem100  42848  fourierdlem103  42851  fourierdlem104  42852  fourierdlem105  42853  fourierdlem108  42856  fourierdlem109  42857  fourierdlem110  42858  fourierdlem112  42860  fourierdlem113  42861  sge0pnffigt  43035  sge0resplit  43045  ovnval2  43184  ovnval2b  43191  ovnlecvr  43197  ovnpnfelsup  43198  ovn0lem  43204  ovnsubaddlem1  43209  hoidmvlelem1  43234  ovnhoilem1  43240  ovnhoi  43242  ovnlecvr2  43249  hoiqssbl  43264  ovolval5lem2  43292  ovolval5lem3  43293  ovolval5  43294  ovnovol  43298  smfsuplem2  43443  smfsup  43445  smfinflem  43448  smfinf  43449  cbvrex2  43659  2reu8i  43669  2reuimp0  43670  afvelrnb  43719  afvelrnb0  43720  elsetpreimafvb  43901  imasetpreimafvbijlemfo  43922  iccelpart  43950  iccpartiun  43951  icceuelpart  43953  sprsymrelf1lem  44008  sprsymrelf  44012  fmtnofac2lem  44085  fmtnofac2  44086  fmtnofac1  44087  m1expevenALTV  44165  odd2np1ALTV  44192  opoeALTV  44201  opeoALTV  44202  mogoldbblem  44238  nfermltlrev  44262  isgbow  44270  isgbo  44271  7gbow  44290  9gbo  44292  11gbo  44293  sbgoldbwt  44295  mogoldbb  44303  sbgoldbo  44305  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  bgoldbtbnd  44327  uspgrsprf1  44375  uspgrsprfo  44376  0nodd  44430  1odd  44431  2nodd  44432  0even  44555  1neven  44556  2even  44557  2zlidl  44558  2zrngamgm  44563  2zrngagrp  44567  2zrngmmgm  44570  2zrngnmrid  44574  lcoval  44821  el0ldep  44875  ldepspr  44882  zlmodzxzldep  44913  line  45146  rrxline  45148