Theorem rexbidv 3297

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3144

This theorem is referenced by:  2rexbidv  3300  rexralbidv  3301  rexeqbi1dvOLD  3418  rexeqbidvOLD  3424  cbvrex2vw  3462  cbvrex2v  3465  rspc2ev  3635  rspc3ev  3637  ceqsrex2v  3651  reuxfr1d  3741  uniiunlem  4061  n0snor2el  4764  eliun  4923  dfiin2g  4957  dfiunv2  4960  dmopab2rex  5786  elrnmpt  5828  elrnmptg  5831  elimag  5933  fvelrnb  6726  fvelimab  6737  foelrn  6872  foco2  6873  elabrex  7002  abrexco  7003  f1oiso  7104  f1oiso2  7105  orduninsuc  7558  funcnvuni  7636  fiunlem  7643  fiun  7644  f1iun  7645  abrexex2g  7665  f1oweALT  7673  el2xptp  7735  tfrlem12  8025  seqomlem2  8087  nneob  8279  qseq2  8344  elqsg  8348  elqsecl  8351  elixpsn  8501  ixpsnf1o  8502  isfi  8533  enfi  8734  pssnn  8736  frfi  8763  unblem1  8770  unblem2  8771  unbnn2  8775  fofinf1o  8799  finsschain  8831  indexfi  8832  elfi  8877  marypha1lem  8897  supeq3  8913  supmo  8916  suplub  8924  supisolem  8937  eqinf  8948  infval  8950  infglb  8954  infglbb  8955  infmo  8959  oieq1  8976  ordtypelem2  8983  ordtypelem3  8984  ordtypelem9  8990  wemaplem1  9010  brwdom2  9037  brwdom3  9046  unwdomg  9048  oemapval  9146  cantnf  9156  wemapwe  9160  cnfcom3clem  9168  tz9.13  9220  tz9.13g  9221  cardf2  9372  isnum2  9374  ennum  9376  cardiun  9411  infxpenc2  9448  aceq1  9543  aceq2  9545  dfac5lem3  9551  dfac5lem4  9552  dfac2a  9555  dfac2b  9556  kmlem9  9584  kmlem12  9587  kmlem14  9589  ackbij1  9660  cflm  9672  cfss  9687  cofsmo  9691  cfsmolem  9692  cfcoflem  9694  coftr  9695  isfin7  9723  fin23lem26  9747  isf32lem5  9779  fin1a2lem11  9832  hsmexlem2  9849  axdc3lem3  9874  axdc3  9876  numthcor  9916  zorn2lem7  9924  brdom3  9950  brdom7disj  9953  brdom6disj  9954  iundom2g  9962  fpwwe2  10065  winainflem  10115  winalim2  10118  inar1  10197  tskuni  10205  nqereu  10351  prnmax  10417  genpv  10421  genpnmax  10429  genpass  10431  prlem936  10469  recexsrlem  10525  map2psrpr  10532  supsrlem  10533  axrrecex  10585  axpre-sup  10591  dedekind  10803  cnegex  10821  recex  11272  fimaxre3  11587  infm3  11600  supaddc  11608  supadd  11609  supmul1  11610  supmullem1  11611  supmullem2  11612  supmul  11613  creur  11632  creui  11633  cju  11634  nnunb  11894  arch  11895  xrsupsslem  12701  xrinfmsslem  12702  xrsupss  12703  xrinfmss  12704  xrub  12706  supxrunb1  12713  supxrunb2  12714  infmremnf  12737  infmrp1  12738  modmuladd  13282  fsequb2  13345  hashge2el2difr  13840  iswrd  13864  wrdval  13865  csbwrdg  13895  cshword  14153  0csh0  14155  2cshwcshw  14187  scshwfzeqfzo  14188  cshimadifsn  14191  shftfval  14429  abs1m  14695  rexfiuz  14707  reusq0  14822  limsupbnd2  14840  clim  14851  rlim  14852  rlim2  14853  rlim0  14865  rlim0lt  14866  ello1mpt2  14879  o1lo1  14894  o1compt  14944  rlimdiv  15002  climsup  15026  sumeq1  15045  sumeq2w  15049  summo  15074  fsum  15077  fsumcvg3  15086  infcvgaux2i  15213  mertenslem1  15240  mertenslem2  15241  mertens  15242  prodeq1f  15262  prodeq2w  15266  prodmo  15290  fprod  15295  divides  15609  odd2np1lem  15689  opeo  15714  omeo  15715  divalglem4  15747  divalglem10  15753  divalg  15754  gcdcllem3  15850  zeqzmulgcd  15859  bezoutlem1  15887  exprmfct  16048  nnnn0modprm0  16143  pythagtriplem2  16154  pythagtrip  16171  pceu  16183  pcprmpw2  16218  unbenlem  16244  4sqlem12  16292  vdwapval  16309  vdwapun  16310  vdwmc2  16315  vdwpc  16316  vdwlem2  16318  vdwlem10  16326  vdwlem13  16329  vdwnnlem1  16331  rami  16351  cshwsiun  16433  cshwrepswhash1  16436  brssc  17084  isdrs  17544  drsdir  17545  drsdirfi  17548  isdrs2  17549  ipodrsima  17775  grprinvlem  17883  gsumvalx  17886  gsumpropd  17888  gsumress  17892  isnsgrp  17905  smndex2dnrinv  18080  sgrp2nmndlem5  18094  grpinvex  18113  dfgrp2  18128  grpidinv2  18158  grpidinv  18159  dfgrp3lem  18197  grp1  18206  imasgrp2  18214  cyccom  18346  conjnmzb  18393  gaorb  18437  orbsta  18443  symgfix2  18544  symgextfo  18550  pmtrprfvalrn  18616  psgnunilem3  18624  psgneu  18634  psgnval  18635  psgnvali  18636  psgnvalii  18637  ispgp  18717  subgpgp  18722  sylow1  18728  pgpfi  18730  sylow2blem3  18747  fislw  18750  sylow3lem2  18753  lsmelvalm  18776  lsmass  18795  pj1fval  18820  pj1val  18821  pj1eu  18822  pj1id  18825  efgrelexlema  18875  efgrelexlemb  18876  efgredeu  18878  cyggeninv  19002  cygablOLD  19011  pgpfac1lem2  19197  pgpfac1lem3  19199  pgpfac1lem4  19200  pgpfac1  19202  pgpfaclem2  19204  pgpfac  19206  dvdsrval  19395  dvdsr  19396  subrgdvds  19549  lss1d  19735  lspsn  19774  lspsnel  19775  lspsolvlem  19914  rspsn  20027  opsrval  20255  znf1o  20698  cygznlem3  20716  psgndiflemA  20745  ellspd  20946  mat1dimelbas  21080  mat1dimbas  21081  scmatval  21113  scmatel  21114  scmateALT  21121  mat0scmat  21147  decpmataa0  21376  decpmatmulsumfsupp  21381  pmatcollpw2lem  21385  pm2mpmhmlem1  21426  chpscmat  21450  basis2  21559  eltg2  21566  tg2  21573  isclo  21695  neival  21710  isnei  21711  isneip  21713  restbas  21766  neitr  21788  cnpval  21844  iscnp  21845  cnpimaex  21864  lmbr  21866  lmbr2  21867  cnprest2  21898  lmff  21909  regsep  21942  pnrmopn  21951  nrmsep3  21963  isnrm2  21966  iscmp  21996  cmpsublem  22007  cmpsub  22008  tgcmp  22009  sscmp  22013  hauscmplem  22014  1stcclb  22052  1stcfb  22053  is2ndc  22054  2ndc1stc  22059  1stcrest  22061  2ndcctbss  22063  1stcelcls  22069  llyeq  22078  nllyeq  22079  hausllycmp  22102  lly1stc  22104  refssex  22119  refun0  22123  islocfin  22125  locfinnei  22131  comppfsc  22140  txbas  22175  ptval  22178  ptpjopn  22220  ptclsg  22223  txcnp  22228  ptcnp  22230  txrest  22239  ptrescn  22247  txcmp  22251  tx1stc  22258  xkococn  22268  kqreglem1  22349  fbasssin  22444  fbssfi  22445  fbssint  22446  fbun  22448  fgss2  22482  fgcl  22486  ufli  22522  fmfnfmlem3  22564  fbflim2  22585  hauspwpwf1  22595  flfneii  22600  flftg  22604  txflf  22614  fclscf  22633  alexsubb  22654  alexsubALT  22659  tsmssubm  22751  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ust0  22828  trust  22838  elutop  22842  ucnval  22886  ucncn  22894  cfiluexsm  22899  cfiluweak  22904  blssps  23034  blss  23035  imasf1oxms  23099  mopni  23102  metss  23118  metrest  23134  metcnp3  23150  cfilucfil  23169  metuel2  23175  nlmvscn  23296  nrginvrcn  23301  icccmplem1  23430  icccmplem2  23431  icccmp  23433  divcn  23476  cncfval  23496  elcncf2  23498  cncfmet  23516  cnheibor  23559  evth  23563  lebnumlem3  23567  lebnum  23568  xlebnum  23569  lebnumii  23570  ipcn  23849  lmmbr  23861  lmmbr2  23862  cfilfval  23867  cfili  23871  iscfil3  23876  caufval  23878  iscau  23879  iscau2  23880  equivcfil  23902  equivcau  23903  lmcau  23916  ovolval  24074  elovolm  24076  ovolgelb  24081  ovoliunlem1  24103  ovoliun2  24107  ovolshftlem1  24110  ovolscalem1  24114  ovolicc  24124  ioombl1lem4  24162  uniioombllem2  24184  mbfaddlem  24261  mbfsup  24265  mbfinf  24266  mbflimsup  24267  i1fmulc  24304  itg1climres  24315  itg2val  24329  itg2l  24330  itg2leub  24335  itg2seq  24343  itg2monolem1  24351  itg2mono  24354  itg2i1fseq2  24357  cniccibl  24441  ellimc3  24477  limciun  24492  dvferm1  24582  dvferm2  24584  lhop1lem  24610  ply1divex  24730  ig1peu  24765  plyval  24783  elply2  24786  coeval  24813  coeeu  24815  coelem  24816  coeeq  24817  plydivlem4  24885  plydivex  24886  aannenlem2  24918  aalioulem2  24922  aaliou2  24929  ulmval  24968  ulm2  24973  ulmcau  24983  ulmdvlem3  24990  abelthlem9  25028  abelth  25029  efif1olem4  25129  eflogeq  25185  efopn  25241  cxpcn3  25329  cxpeq  25338  rlimcnp  25543  lgamgulmlem6  25611  muval  25709  dchrptlem1  25840  dchrptlem2  25841  lgsdchrval  25930  2lgslem1b  25968  addsq2nreurex  26020  pntpbnd  26164  pntibndlem3  26168  pntibnd  26169  pntlemi  26180  pntleme  26184  pntlemp  26186  pnt3  26188  istrkgld  26245  istrkg3ld  26247  axtgsegcon  26250  axtgpasch  26253  axtgcont1  26254  axtgupdim2  26257  legov  26371  islnopp  26525  ishpg  26545  hpgbr  26546  hpgcom  26553  iscgra1  26596  isinag  26624  isleag  26633  ttgval  26661  ttgitvval  26668  ttgelitv  26669  brbtwn  26685  brcgr  26686  axpasch  26727  axlowdim2  26746  axlowdim  26747  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  upgredg2vtx  26926  edglnl  26928  usgredg4  26999  ushgredgedg  27011  ushgredgedgloop  27013  dfnbgr2  27119  nbgrel  27122  nbumgrvtx  27128  nbgrnself  27141  uvtxel1  27178  cusgrfilem2  27238  cusgrfi  27240  vtxd0nedgb  27270  fusgrn0degnn0  27281  wlkonl1iedg  27447  wspniunwspnon  27702  elwwlks2on  27738  clwwlknscsh  27841  erclwwlkneq  27846  eleclclwwlkn  27855  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  3cyclfrgrrn1  28064  friendshipgt3  28177  isgrpo  28274  isgrpoi  28275  grpoidinvlem3  28283  grpoideu  28286  grpoidinv2  28292  nmoofval  28539  nmooval  28540  nmosetn0  28542  nmoolb  28548  nmoubi  28549  nmlno0lem  28570  chcompl  29019  pjhthmo  29079  pjhval  29174  pjpreeq  29175  h1de2ci  29333  elspansn  29343  nmopval  29633  nmopsetn0  29642  nmfnval  29653  nmfnsetn0  29655  eigvecval  29673  hhcno  29681  hhcnf  29682  nmoplb  29684  nmopub  29685  nmfnlb  29701  nmfnleub  29702  eleigvec  29734  nmlnop0iALT  29772  nmopun  29791  nmcexi  29803  branmfn  29882  pjnmopi  29925  cvbr  30059  hatomic  30137  chrelat2  30147  cdjreui  30209  cdj3lem2  30212  elabreximd  30270  br8d  30361  unipreima  30391  abfmpunirn  30397  curry2ima  30444  toslublem  30654  tosglblem  30656  cyc3genpm  30794  archirng  30817  archiexdiv  30819  archiabllem2a  30823  archiabl  30827  isarchiofld  30890  elgrplsmsn  30944  mxidlprm  30977  fedgmul  31027  ccfldextdgrr  31057  crefi  31111  pcmplfin  31124  pstmfval  31136  tpr2rico  31155  rge0scvg  31192  ismntop  31267  esumc  31310  esumpcvgval  31337  esum2dlem  31351  inelsros  31437  diffiunisros  31438  dya2icoseg2  31536  dya2iocuni  31541  eulerpartlemgvv  31634  eulerpartlemgh  31636  hgt749d  31920  tgoldbachgt  31934  bnj66  32132  bnj873  32196  bnj18eq1  32199  bnj1234  32285  bnj1318  32297  cplgredgex  32367  subfacp1lem3  32429  pconncn  32471  cnpconn  32477  txpconn  32479  connpconn  32482  iscvm  32506  cvmcov  32510  cvmopnlem  32525  cvmliftlem15  32545  cvmlift3lem2  32567  cvmlift3lem4  32569  cvmlift3  32575  satf  32600  satfv1  32610  satfvsucsuc  32612  satfbrsuc  32613  satfrnmapom  32617  satf0op  32624  sat1el2xp  32626  fmlafvel  32632  fmlasuc  32633  fmla1  32634  isfmlasuc  32635  fmlaomn0  32637  fmlasucdisj  32646  satffunlem1lem1  32649  satffunlem1lem2  32650  satffunlem2lem1  32651  dmopab3rexdif  32652  satffunlem2lem2  32653  sategoelfvb  32666  satfv1fvfmla1  32670  2goelgoanfmla1  32671  br8  32992  br6  32993  br4  32994  dfrdg2  33040  dfrdg3  33041  orderseqlem  33094  poseq  33095  soseq  33096  elno  33153  sltval  33154  noprefixmo  33202  nosupno  33203  nosupdm  33204  nosupfv  33206  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem3  33210  nosupbnd1lem4  33211  nosupbnd1lem5  33212  noeta  33222  altxpeq2  33435  funtransport  33492  fvtransport  33493  brcolinear2  33519  colineardim1  33522  segcon2  33566  brsegle  33569  funray  33601  fvray  33602  funline  33603  linedegen  33604  fvline  33605  ellines  33613  nn0prpwlem  33670  fnessref  33705  neibastop2lem  33708  neibastop2  33709  tailfb  33725  unblimceq0lem  33845  unblimceq0  33846  unbdqndv2  33850  bj-finsumval0  34570  relowlssretop  34647  nlpineqsn  34692  pibp19  34698  phpreu  34891  matunitlindflem2  34904  ptrest  34906  poimirlem4  34911  poimirlem17  34924  poimirlem20  34927  poimirlem24  34931  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem31  34938  poimirlem32  34939  poimir  34940  heicant  34942  mblfinlem1  34944  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  itg2gt0cn  34962  cnicciblnc  34978  ftc1anclem6  34987  unirep  35003  indexa  35023  sdclem2  35032  sdclem1  35033  sdc  35034  fdc  35035  fdc1  35036  incsequz  35038  istotbnd  35062  sstotbnd2  35067  equivtotbnd  35071  isbnd  35073  bndss  35079  ssbnd  35081  totbndbnd  35082  ismtybndlem  35099  heibor1lem  35102  heiborlem1  35104  heiborlem6  35109  heiborlem8  35111  heiborlem10  35113  heibor  35114  rngoid  35195  isgrpda  35248  isdrngo2  35251  divrngidl  35321  prnc  35360  isfldidl  35361  exanres3  35568  brcoels  35695  br1cossxrnres  35703  eldm1cossres2  35716  prtlem5  36011  prtlem13  36019  prtlem16  36020  islshp  36130  lsmsat  36159  lcvbr  36172  lsatcv0  36182  lshpsmreu  36260  lshpkrlem1  36261  lshpkrlem2  36262  lshpkrlem3  36263  lshpkrcl  36267  lshpset2N  36270  islshpkrN  36271  cvrval  36420  atlex  36467  glbconxN  36529  hlsuprexch  36532  islln  36657  islpln  36681  islpln5  36686  lvolex3N  36689  islvol  36724  islvol5  36730  ispointN  36893  pmapglbx  36920  paddval  36949  elpaddn0  36951  elpaddat  36955  elpadd0  36960  4atex  37227  4atex2  37228  cdlemefrs29bpre1  37548  cdlemefrs32fva  37551  cdlemg33b  37858  dvhb1dimN  38137  dvhopellsm  38268  dib1dim  38316  diclspsn  38345  dihglblem2aN  38444  dihglblem2N  38445  dih1dimatlem  38480  dvh3dimatN  38590  dvh2dim  38596  dvh3dim  38597  dvh4dimN  38598  dvh3dim3N  38600  dochfl1  38627  lcfl7N  38652  lcf1o  38702  lcfrlem39  38732  mapdpglem3  38826  hvmapvalvalN  38912  hdmap14lem2a  39018  hdmapglem7a  39078  3rspcedvd  39125  nnn1suc  39179  prjspeclsp  39282  elrfi  39311  isnacs  39321  nacsfg  39322  nacsfix  39329  mzpcompact2lem  39368  eldiophb  39374  eldioph  39375  eldioph2  39379  eldioph2b  39380  eldioph3  39383  eldiophss  39391  diophrex  39392  sbcrexgOLD  39402  sbc2rexgOLD  39405  rexrabdioph  39411  rexfrabdioph  39412  elnn0rabdioph  39420  dvdsrabdioph  39427  eldioph4b  39428  eldioph4i  39429  diophren  39430  rencldnfilem  39437  pell1234qrdich  39478  jm2.27  39625  expdiophlem1  39638  wepwsolem  39662  aomclem8  39681  islnr3  39735  lnr2i  39736  lpirlnr  39737  hbtlem1  39743  hbtlem2  39744  hbtlem7  39745  hbtlem4  39746  hbtlem5  39748  hbtlem6  39749  dgraaval  39764  dgraalem  39765  dgraaub  39768  rngunsnply  39793  brtrclfv2  40092  clsk1indlem1  40415  extoimad  40535  mnuop123d  40618  mnuop23d  40622  mnuprdlem1  40628  mnuprdlem2  40629  elabrexg  41323  foelrnf  41467  disjrnmpt2  41469  upbdrech  41592  ssfiunibd  41596  supxrgere  41621  supxrgelem  41625  supxrge  41626  suplesup  41627  infxr  41655  infleinf  41660  supxrunb3  41692  unb2ltle  41709  uzub  41725  supminfxr  41760  iccshift  41814  iooshift  41818  climinf  41907  climinff  41912  ellimcabssub0  41918  climf  41923  limcperiod  41929  limclner  41952  climf2  41967  clim2d  41974  limsuppnfd  42003  limsuppnf  42012  climinfmpt  42016  limsupubuzmpt  42020  limsupmnf  42022  limsupre2lem  42025  limsupre2  42026  limsupmnfuz  42028  limsupre2mpt  42031  limsupre3lem  42033  limsupre3  42034  limsupre3mpt  42035  limsupre3uzlem  42036  limsupre3uz  42037  limsupreuz  42038  limsupreuzmpt  42040  climuz  42045  liminfreuzlem  42103  liminfreuz  42104  xlimmnfvlem1  42133  xlimmnfv  42135  xlimpnfvlem1  42137  xlimpnfv  42139  cncfshiftioo  42195  fperdvper  42223  itgiccshift  42285  itgperiod  42286  stoweidlem27  42332  stoweidlem31  42336  stoweidlem43  42348  stoweidlem46  42351  stoweidlem52  42357  stoweidlem60  42365  fourierdlem42  42454  fourierdlem48  42459  fourierdlem51  42462  fourierdlem54  42465  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem68  42479  fourierdlem70  42481  fourierdlem71  42482  fourierdlem73  42484  fourierdlem80  42491  fourierdlem81  42492  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem92  42503  fourierdlem96  42507  fourierdlem97  42508  fourierdlem98  42509  fourierdlem99  42510  fourierdlem100  42511  fourierdlem103  42514  fourierdlem104  42515  fourierdlem105  42516  fourierdlem108  42519  fourierdlem109  42520  fourierdlem110  42521  fourierdlem112  42523  fourierdlem113  42524  sge0pnffigt  42698  sge0resplit  42708  ovnval2  42847  ovnval2b  42854  ovnlecvr  42860  ovnpnfelsup  42861  ovn0lem  42867  ovnsubaddlem1  42872  hoidmvlelem1  42897  ovnhoilem1  42903  ovnhoi  42905  ovnlecvr2  42912  hoiqssbl  42927  ovolval5lem2  42955  ovolval5lem3  42956  ovolval5  42957  ovnovol  42961  smfsuplem2  43106  smfsup  43108  smfinflem  43111  smfinf  43112  cbvrex2  43322  2reu8i  43332  2reuimp0  43333  afvelrnb  43382  afvelrnb0  43383  elsetpreimafvb  43564  imasetpreimafvbijlemfo  43585  iccelpart  43613  iccpartiun  43614  icceuelpart  43616  sprsymrelf1lem  43673  sprsymrelf  43677  fmtnofac2lem  43750  fmtnofac2  43751  fmtnofac1  43752  m1expevenALTV  43832  odd2np1ALTV  43859  opoeALTV  43868  opeoALTV  43869  mogoldbblem  43905  nfermltlrev  43929  isgbow  43937  isgbo  43938  7gbow  43957  9gbo  43959  11gbo  43960  sbgoldbwt  43962  mogoldbb  43970  sbgoldbo  43972  nnsum3primesgbe  43977  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  bgoldbtbnd  43994  uspgrsprf1  44042  uspgrsprfo  44043  0nodd  44097  1odd  44098  2nodd  44099  0even  44222  1neven  44223  2even  44224  2zlidl  44225  2zrngamgm  44230  2zrngagrp  44234  2zrngmmgm  44237  2zrngnmrid  44241  lcoval  44487  el0ldep  44541  ldepspr  44548  zlmodzxzldep  44579  line  44739  rrxline  44741