Theorem ralbidv 3147

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 473	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3146	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 198   ∈ wcel 2050  ∀wral 3088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ral 3093

This theorem is referenced by:  2ralbidv  3149  rexralbidv  3246  raleqbi1dvOLD  3357  raleqbidvOLD  3363  cbvral2v  3392  rspceaimv  3543  rspc2  3546  rspc2v  3548  rspc3v  3551  reu6i  3633  reu7  3637  sbcralt  3760  reu8nf  3765  raaan  4344  raaanv  4345  raaan2  4348  2reu4lem  4349  reusngf  4487  2ralsng  4491  rexreusng  4492  reuprg0  4513  issn  4638  2ralunsn  4700  elintg  4758  elintrabg  4763  eliin  4798  disjprg  4926  disjxun  4928  brralrspcev  4990  reusv2lem2  5154  reusv3  5160  poeq1  5330  somo  5363  frirr  5385  fr2nr  5386  frminex  5388  wereu2  5405  posn  5488  frsn  5490  ralxpf  5568  cnvpo  5978  reu3op  5983  reuop  5984  fnmptfvd  6638  iinpreima  6664  dff4  6692  dff13f  6841  fpropnf1  6852  eusvobj2  6971  ovanraleqv  7002  f1opr  7031  ofreq  7232  sorpssuni  7278  sorpssint  7279  fr3nr  7312  onssmin  7330  funcnvuni  7453  f1oweALT  7487  frxp  7627  wrecseq123  7753  wfrlem1  7759  wfrlem3a  7762  wfrlem15  7775  smoeq  7793  tfrlem12  7831  tz7.48lem  7882  elixp2  8265  undifixp  8297  xpf1o  8477  nneneq  8498  ac6sfi  8559  frfi  8560  fipreima  8627  indexfi  8629  marypha1lem  8694  marypha1  8695  supeq1  8706  supeq3  8710  supmo  8713  eqsup  8717  supub  8720  suplub  8721  sup0  8727  supisoex  8735  eqinf  8745  infval  8747  infmo  8756  oieq1  8773  ordtypecbv  8778  ordtypelem3  8781  ordtypelem6  8784  ordtypelem7  8785  ordtypelem9  8787  wemaplem1  8807  wemaplem2  8808  zfregcl  8855  oemapval  8942  oemapvali  8943  cantnf  8952  wemapwe  8956  rankval3b  9051  unbndrank  9067  rankunb  9075  rankuni2b  9078  tcrank  9109  scottex  9110  scottexs  9112  scott0s  9113  bnd2  9118  updjud  9159  dfac8clem  9254  ac5num  9258  acni  9267  acni2  9268  alephval3  9332  dfac4  9344  dfac5lem5  9349  dfac5  9350  dfac2a  9351  dfac2b  9352  dfacacn  9363  kmlem2  9373  kmlem13  9384  cflem  9468  cflecard  9475  cfeq0  9478  cfsuc  9479  cfflb  9481  cofsmo  9491  cfsmolem  9492  cfcoflem  9494  coftr  9495  alephsing  9498  fin23lem11  9539  isfin3ds  9551  fin23lem17  9560  fin23lem39  9572  isf33lem  9588  isf34lem6  9602  fin1a2lem13  9634  hsmexlem4  9651  hsmex  9654  axcc2lem  9658  axcc3  9660  dcomex  9669  axdc2lem  9670  axdc3lem2  9673  axdc3lem3  9674  axdc3  9676  axdc4lem  9677  axcclem  9679  zorn2lem2  9719  zorn2lem7  9724  zorn2g  9725  zornn0g  9727  ttukeylem7  9737  axdclem2  9742  brdom3  9750  brdom7disj  9753  brdom6disj  9754  alephval2  9794  inar1  9997  axgroth6  10050  pinq  10149  nqereu  10151  prlem934  10255  supexpr  10276  supsrlem  10333  axpre-sup  10391  dedekind  10605  dedekindle  10606  fiminreOLD  11393  lbreu  11394  sup2  11400  infm3  11403  nnsub  11487  uzwo  12128  nnwof  12131  ublbneg  12150  lbzbi  12153  zsupss  12154  uzsupss  12157  uzwo3  12160  zmax  12162  rpnnen1lem1  12195  rpnnen1lem3  12196  rpnnen1lem4  12197  rpnnen1lem5  12198  xrsupsslem  12519  xrinfmsslem  12520  xrsupss  12521  xrinfmss  12522  flval2  13002  axdc4uzlem  13169  ssnn0fi  13171  fsuppmapnn0fiubex  13178  faclbnd4lem4  13474  bccl  13500  hashgt12el  13599  hashbc  13627  hashge2el2dif  13652  wrdind  13918  wrdindOLD  13919  wrd2ind  13920  wrd2indOLD  13921  rexanre  14570  rexico  14577  cau4  14580  reusq0  14686  clim  14715  rlim  14716  rlim2  14717  clim2  14725  clim2c  14726  clim0c  14728  rlim0  14729  rlim0lt  14730  ello12r  14738  ello1d  14744  elo12r  14749  rlimresb  14786  rlimcld2  14799  climabs0  14806  rlimo1  14837  lo1add  14847  lo1mul  14848  isercoll  14888  incexclem  15054  sqrt2irr  15465  gcdcllem1  15711  gcdcllem2  15712  dfgcd2  15753  fissn0dvds  15822  dvdslcmf  15834  lcmfledvds  15835  lcmf  15836  lcmfunsnlem1  15840  lcmfunsnlem2lem1  15841  lcmfunsnlem  15844  lcmfdvds  15845  reumodprminv  16000  pc2dvds  16074  pcz  16076  prmpwdvds  16099  infpn2  16108  prmreclem2  16112  prmreclem3  16113  prmreclem5  16115  prmreclem6  16116  vdwlem6  16181  vdwlem8  16183  vdwlem13  16188  vdwnnlem1  16190  vdwnn  16193  ramcl  16224  cshwrepswhash1  16295  prdsleval  16609  imasval  16643  imasaddfnlem  16660  imasvscafn  16669  mrisval  16762  isacs  16783  isacs2  16785  isacs1i  16789  mreacs  16790  acsfn  16791  acsfn2  16795  iscatd  16805  catidex  16806  catideu  16807  cidval  16809  catidd  16812  comfeq  16837  catpropd  16840  ismon  16864  isfunc  16995  isnat  17078  isinito  17121  istermo  17122  isprs  17401  drsdirfi  17409  ispos  17418  lubfval  17449  lubeldm  17452  lubval  17455  lubprop  17457  lublecllem  17459  glbfval  17462  glbeldm  17465  glbval  17468  glbprop  17470  joinval2lem  17479  joinlem  17482  meetval2lem  17493  meetlem  17496  isglbd  17588  lubl  17591  lubun  17594  clatleglb  17597  poslubmo  17617  posglbmo  17618  poslubd  17619  ipodrsima  17636  isdlat  17664  mgm1  17728  gsumval2  17751  sgrp1  17764  mhmima  17834  mndind  17837  gsumwspan  17855  sgrp2rid2  17885  sgrp2rid2ex  17886  sgrp2nmndlem4  17887  dfgrp2  17919  isgrpinv  17946  grpidinv  17949  dfgrp3lem  17987  issubg4  18085  0subg  18091  cycsubgcl  18092  isnsg2  18096  nsgacs  18102  elnmz  18105  ghmrn  18145  ghmnsgima  18156  isga  18195  orbsta  18217  cntzfval  18224  elcntz  18226  resscntz  18236  oppgsubg  18265  symgextfo  18314  gsmsymgreqlem2  18323  gsmsymgreq  18324  pmtrdifel  18372  pmtrdifwrdellem3  18375  pmtrdifwrdel2  18378  psgnunilem2  18388  psgnunilem3  18389  odeq  18443  gexid  18470  gexlem2  18471  gexdvds  18473  isslw  18497  sylow2alem1  18506  sylow2alem2  18507  efgval  18604  efgrelexlemb  18639  efgcpbllemb  18644  abl1  18745  dmdprd  18873  dprd2da  18917  pgpfac1lem5  18954  ring1  19078  isabv  19315  islss  19431  lssacs  19464  reslmhm  19549  islbs  19573  pj1lmhm  19597  lbsacsbs  19653  isrrg  19785  opsrval  19971  ply1coe  20170  cply1coe0bi  20174  zringlpir  20341  psgndiflemA  20450  ocvfval  20515  elocv  20517  iunocv  20530  frlmlbs  20646  islindf  20661  islinds2  20662  islindf2  20663  lindfrn  20670  lsslindf  20679  islindf4  20687  mat0dimcrng  20786  mdetunilem1  20928  mdetunilem9  20936  cpmat  21024  cpmatel  21026  1elcpmat  21030  m2cpminvid2lem  21069  basgen2  21304  bastop1  21308  isclo  21402  ordtbaslem  21503  iscn  21550  cnpval  21551  iscnp  21552  iscnp3  21559  lmbr  21573  lmbr2  21574  lmbrf  21575  cnprest  21604  cnprest2  21605  t0sep  21639  isreg  21647  t1sep2  21684  tgcmp  21716  1stcclb  21759  1stcfb  21760  2ndc1stc  21766  1stcrest  21768  2ndcdisj  21771  islly  21783  isnlly  21784  lly1stc  21811  isref  21824  islocfin  21832  elkgen  21851  kgencn  21871  elpt  21887  elptr  21888  ptcnplem  21936  tx1stc  21965  cnmpt21  21986  kqt0lem  22051  isr0  22052  regr1lem2  22055  r0sep  22063  nrmr0reg  22064  flffbas  22310  cnflf  22317  cnflf2  22318  lmflf  22320  txflf  22321  fclsopni  22330  fclsnei  22334  fclsrest  22339  fcfnei  22350  cnfcf  22357  alexsubb  22361  alexsubALTlem3  22364  qustgplem  22435  tsmsfbas  22442  tsmsres  22458  tsmsf1o  22459  tsmsxplem1  22467  ustval  22517  isust  22518  ustincl  22522  ustdiag  22523  ustinvel  22524  ustexhalf  22525  ust0  22534  utopval  22547  ucnval  22592  isucn  22593  isucn2  22594  ucnima  22596  iscfilu  22603  ispsmet  22620  ismet  22639  isxmet  22640  imasdsf1olem  22689  imasf1oxmet  22691  imasf1omet  22692  metss  22824  met1stc  22837  prdsxmslem2  22845  txmetcnp  22863  metucn  22887  tngngp3  22971  nlmvscn  23002  nmoval  23030  nmolb  23032  qtopbaslem  23073  cncfval  23202  elcncf2  23204  mulc1cncf  23219  cncfmet  23222  evth  23269  lebnumlem3  23273  lebnum  23274  xlebnum  23275  ishtpy  23282  isphtpy  23291  pi1xfr  23365  pi1coghm  23371  isclmp  23407  ipcn  23555  lmmbr2  23568  lmmbr3  23569  lmmbrf  23571  cfilfval  23573  iscfil  23574  fmcfil  23581  caufval  23584  iscau  23585  iscau2  23586  iscau3  23587  iscau4  23588  iscauf  23589  caucfil  23592  cfilresi  23604  causs  23607  lmclim  23612  cmetcusp1  23662  minveclem4c  23734  minveclem2  23735  minveclem3b  23737  minveclem4  23741  minveclem6  23743  minveclem7  23744  ovolicc2lem3  23826  ismbl  23833  dyadmax  23905  dyadmbllem  23906  dyadmbl  23907  opnmbllem  23908  ismbf1  23931  ismbf  23935  mbfeqalem2  23949  mbflimsup  23973  mbfi1fseqlem6  24027  mbfi1flimlem  24029  itg2seq  24049  itg2monolem1  24057  isibl  24072  ply1divex  24436  fta1g  24467  dgrco  24571  plydivex  24592  fta1  24603  vieta1  24607  aannenlem1  24623  aannenlem2  24624  aalioulem2  24628  aalioulem3  24629  ulmval  24674  ulm2  24679  ulmi  24680  ulmres  24682  ulmshftlem  24683  ulmcaulem  24688  ulmcau  24689  ulmss  24691  ulmbdd  24692  ulmdvlem1  24694  ulmdvlem3  24696  pilem2  24746  pilem3  24747  cxpcn3  25033  dmarea  25240  rlimcnp  25248  scvxcvx  25268  lgamgulmlem2  25312  lgamgulmlem3  25313  lgamgulmlem5  25315  lgambdd  25319  lgamcvglem  25322  isppw2  25397  perfectlem2  25511  2sqlem6  25704  2sqlem10  25709  addsq2reu  25721  2sqreulem1  25727  2sqreunnlem1  25730  dchrisumlema  25769  dchrisumlem2  25771  dchrisumlem3  25772  pntpbnd  25869  pntibndlem3  25873  pntibnd  25874  pntleme  25889  pntlem3  25890  pntlemp  25891  pnt3  25893  istrkgld  25950  axtg5seg  25956  tgcgr4  26022  perpln1  26201  perpln2  26202  isperp  26203  brbtwn2  26397  colinearalg  26402  axsegconlem1  26409  axsegcon  26419  ax5seglem4  26424  ax5seglem5  26425  axlowdim  26453  axeuclidlem  26454  axcontlem1  26456  axcontlem2  26457  axcontlem4  26459  axcontlem5  26460  axcontlem8  26463  axcontlem12  26467  elntg2  26477  uvtxusgr  26890  rgrx0ndm  27081  ewlksfval  27089  wksfval  27097  wwlks  27324  wlkiswwlks2  27364  clwwlk  27492  1conngr  27726  frgrwopregasn  27853  frgrwopregbsn  27854  frgrwopreglem5ALT  27859  frgrregord013  27955  isgrpo  28054  isgrpoi  28055  grpoideu  28066  grpoidinv2  28072  vciOLD  28118  isvclem  28134  cnidOLD  28139  isnvlem  28167  nvi  28171  lnoval  28309  islno  28310  isblo3i  28358  blo3i  28359  blocnilem  28361  ajfval  28366  ubthlem1  28428  ubthlem2  28429  ubthlem3  28430  ubth  28431  minvecolem2  28433  minvecolem3  28434  minvecolem4c  28437  minvecolem4  28438  minvecolem5  28439  minvecolem6  28440  minvecolem7  28441  h2hcau  28538  h2hlm  28539  hilid  28720  hcau  28743  hlimi  28747  hlim2  28751  ocel  28842  adjsym  29394  ellnop  29419  ellnfn  29444  hhcno  29465  hhcnf  29466  lnopeq  29570  elunop2  29574  lnophm  29580  lnconi  29594  lnopcnbd  29597  lnfncnbd  29618  imaelshi  29619  riesz3i  29623  riesz4i  29624  riesz4  29625  riesz1  29626  cnlnadjlem2  29629  cnlnadjlem5  29632  cnlnadjlem8  29635  cnlnadji  29637  nmopadjlei  29649  cnvbraval  29671  leopg  29683  leoppos  29687  mdbr  29855  dmdbr  29860  cdj3i  30002  disjunsn  30113  funcnv5mpt  30178  fgreu  30182  fcnvgreu  30183  xrge0infss  30239  resspos  30378  isomnd  30420  inftmrel  30475  isinftm  30476  archiabl  30493  isarchiofld  30569  0nellinds  30608  lindssn  30610  crefeq  30753  esum2d  30996  sigaval  31014  issgon  31027  isrnmeas  31104  ismbfm  31155  isanmbfm  31159  mbfmcst  31162  elcarsg  31208  sitgval  31235  eulerpartlemd  31269  ballotleme  31400  tgoldbachgt  31582  bnj1185  31713  bnj1385  31752  bnj66  31779  bnj106  31787  bnj155  31798  bnj852  31840  bnj893  31847  bnj1228  31928  bnj1234  31930  bnj1463  31972  derangenlem  32003  subfacp1lem3  32014  subfacp1lem5  32016  subfacp1lem6  32017  subfacp1  32018  erdszelem8  32030  kur14  32048  cnpconn  32062  resconn  32078  cvmscbv  32090  iscvm  32091  cvmsi  32097  cvmsval  32098  cvmlift3lem2  32152  snmlval  32163  mclsssvlem  32329  mclsval  32330  mclsax  32336  mclsind  32337  dfpo2  32511  dfon2lem9  32556  dfrdg2  32561  dfrdg3  32562  frpomin  32599  poseq  32616  soseq  32617  frecseq123  32640  frrlem1  32644  frrlem13  32656  sltval  32675  noprefixmo  32723  nosupno  32724  nosupdm  32725  nosupfv  32727  nosupres  32728  nosupbnd1lem1  32729  nosupbnd1lem3  32731  nosupbnd1lem5  32733  noetalem5  32742  noeta  32743  nocvxminlem  32768  brsslt  32775  conway  32785  etasslt  32795  slerec  32798  fwddifnval  33145  nn0prpwlem  33191  isfne  33208  isfne4  33209  isfne2  33211  isfne3  33212  neibastop3  33231  topmeet  33233  topjoin  33234  filnetlem4  33250  unblimceq0lem  33365  unblimceq0  33366  unbdqndv2  33370  taupilemrplb  34043  csbwrecsg  34050  fin2so  34320  lindsadd  34326  matunitlindflem2  34330  ptrecube  34333  poimirlem2  34335  poimirlem3  34336  poimirlem4  34337  poimirlem24  34357  poimirlem25  34358  poimirlem26  34359  poimirlem27  34360  poimirlem28  34361  poimirlem29  34362  poimirlem30  34363  poimirlem32  34365  poimir  34366  heicant  34368  mblfinlem1  34370  mblfinlem2  34371  voliunnfl  34377  volsupnfl  34378  mbfresfi  34379  itg2addnc  34387  upixp  34446  indexdom  34451  filbcmb  34457  sdclem2  34459  fdc  34462  lmclim2  34475  caures  34477  istotbnd  34489  istotbnd3  34491  sstotbnd  34495  isbnd  34500  heibor  34541  bfp  34544  rrncmslem  34552  isgrpda  34675  idlval  34733  isidl  34734  0idl  34745  unichnidl  34751  pridl  34757  ismaxidl  34760  smprngopr  34772  igenval2  34786  prnc  34787  ispridlc  34790  scottexf  34890  scott0f  34891  riotasvd  35537  islfl  35641  eqlkr  35680  eqlkr3  35682  glbconN  35958  hlsuprexch  35962  ispsubsp  36326  ldilset  36690  isldil  36691  dilsetN  36734  isdilN  36735  trlset  36742  trlval  36743  cdleme27b  36949  cdleme29b  36956  cdleme31so  36960  cdleme31sn1  36962  cdleme31sn1c  36969  cdleme31fv  36971  cdleme40v  37050  istendo  37341  cdlemkid3N  37514  cdlemkid4  37515  cdlemkid5  37516  dihfval  37812  dihval  37813  islpolN  38064  hdmapffval  38407  hdmapfval  38408  hdmapval  38409  hdmapval2lem  38412  hgmapffval  38466  hgmapfval  38467  hgmapval  38468  hgmapvs  38472  qsalrel  38570  isnacs  38696  isnacs2  38698  nacsfix  38704  mzpclval  38717  elmzpcl  38718  rencldnfilem  38813  infmrgelbi  38871  pellfundre  38874  pellfundlb  38877  wepwsolem  39038  fnwe2lem2  39047  aomclem8  39057  dfac11  39058  gicabl  39095  islnr3  39111  hbtlem2  39120  hbtlem5  39124  fiinfi  39294  clsk1independent  39759  ntrclsk13  39784  gneispacess2  39859  imo72b2lem0  39880  imo72b2lem2  39882  imo72b2lem1  39886  imo72b2  39890  scottelrankd  39958  mnuop23d  39977  evth2f  40691  evthf  40703  fnchoice  40705  uzwo4  40735  wessf1ornlem  40870  disjinfi  40879  rnmptlb  40942  rnmptbdd  40944  rnmptbd2  40950  rnmptbd  40957  dstregt0  40977  upbdrech2  41005  fiminre2  41076  rexabslelem  41124  rexabsle  41125  uzub  41137  infrpgernmpt  41173  mccl  41311  ellimcabssub0  41330  climf  41335  clim2f  41349  limsupre  41354  clim2cf  41363  clim0cf  41367  climf2  41379  clim2f2  41383  clim2d  41386  limsupref  41398  limsupbnd1f  41399  limsuppnfd  41415  climinf2  41420  limsuppnf  41424  climinfmpt  41428  climinf3  41429  limsupubuzmpt  41432  limsupmnf  41434  limsupre2lem  41437  limsupre2  41438  limsupmnfuzlem  41439  limsupmnfuz  41440  limsupre2mpt  41443  limsupre3lem  41445  limsupre3  41446  limsupre3mpt  41447  limsupre3uz  41449  limsupreuz  41450  limsupreuzmpt  41452  climuz  41457  liminfreuzlem  41515  liminfreuz  41516  cnrefiisplem  41542  xlimmnfvlem1  41545  xlimmnfv  41547  xlimpnfvlem1  41549  xlimpnfv  41551  xlimmnfmpt  41556  xlimpnfmpt  41557  cncfshift  41588  cncfperiod  41593  fperdvper  41634  dvbdfbdioo  41646  ioodvbdlimc1lem2  41648  ioodvbdlimc2lem  41650  dvnprodlem3  41664  stoweidlem5  41722  stoweidlem9  41726  stoweidlem15  41732  stoweidlem16  41733  stoweidlem27  41744  stoweidlem28  41745  stoweidlem31  41748  stoweidlem34  41751  stoweidlem37  41754  stoweidlem46  41763  stoweidlem48  41765  stoweidlem51  41768  stoweidlem52  41769  stoweidlem59  41776  wallispilem3  41784  stirlinglem13  41803  fourierdlem2  41826  fourierdlem3  41827  fourierdlem16  41840  fourierdlem20  41844  fourierdlem21  41845  fourierdlem22  41846  fourierdlem25  41849  fourierdlem39  41863  fourierdlem42  41866  fourierdlem54  41877  fourierdlem64  41887  fourierdlem77  41900  fourierdlem83  41906  fourierdlem103  41926  fourierdlem104  41927  subsaliuncllem  42072  iundjiun  42174  meaiunincf  42197  caragenval  42207  isome  42208  caragenel  42209  omessle  42212  ovnlerp  42276  hoidmvlelem3  42311  hoidmvle  42314  issmflem  42436  issmfgt  42465  smfmullem2  42499  smfmullem4  42501  smfmul  42502  smfsuplem2  42518  smfsup  42520  smfinflem  42523  smfinf  42524  cbvral2  42708  2reu8i  42719  2reuimp0  42720  dfdfat2  42734  iccpart  42949  iccpartigtl  42956  paireqne  43042  reupr  43053  perfectALTVlem2  43256  bgoldbachlt  43347  tgoldbachlt  43350  isomgreqve  43359  isomushgr  43360  isomuspgrlem2  43367  isomgrsym  43370  isomgrtr  43373  ushrisomgr  43375  upwlksfval  43379  mgmhmima  43438  lidlmsgrp  43562  lidlrng  43563  uzlidlring  43565  ply1mulgsumlem1  43808  ply1mulgsumlem2  43809  linindslinci  43871  lindslinindsimp1  43880  lindslinindsimp2lem5  43885  lindslinindsimp2  43886  linds0  43888  lindsrng01  43891  snlindsntor  43894  lmod1  43915  ldepsnlinc  43931  bigoval  43978  elbigo2r  43982  nn0sumshdiglem2  44051  eenglngeehlnmlem1  44093  eenglngeehlnmlem2  44094  setrec1lem2  44159