Theorem raleqbidv 3329

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2129, ax-11 2146, and ax-12 2166 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)

Hypotheses

Ref	Expression
raleqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
raleqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
raleqbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem raleqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eleq2d 2811	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	imbi12d 343	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))
5	4	ralbidv2 3163	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802  df-ral 3051

This theorem is referenced by:  rspc2vd  3940  frd  5637  f12dfv  7282  f13dfv  7283  knatar  7364  ofrfvalg  7693  fmpox  8072  ovmptss  8098  frrlem4  8295  on2ind  8690  on3ind  8691  marypha1lem  9458  supeq123d  9475  oieq1  9537  acneq  10068  isfin1a  10317  fpwwe2cbv  10655  fpwwe2lem2  10657  fpwwecbv  10669  fpwwelem  10670  eltskg  10775  elgrug  10817  cau3lem  15337  rlim  15475  ello1  15495  elo1  15506  caurcvg2  15660  caucvgb  15662  fsum2dlem  15752  fsumcom2  15756  fprod2dlem  15960  fprodcom2  15964  pcfac  16871  vdwpc  16952  rami  16987  prmgaplem7  17029  prdsval  17440  ismre  17573  isacs2  17636  acsfiel  17637  iscat  17655  iscatd  17656  catidex  17657  catideu  17658  cidfval  17659  cidval  17660  catlid  17666  catrid  17667  comfeq  17689  catpropd  17692  monfval  17718  issubc  17824  fullsubc  17839  isfunc  17853  funcpropd  17892  isfull  17902  isfth  17906  fthpropd  17913  natfval  17939  initoval  17985  termoval  17986  isposd  18318  lubfval  18345  glbfval  18358  ismgm  18604  mgmpropd  18614  ismgmd  18615  issstrmgm  18616  grpidval  18624  gsumvalx  18639  gsumpropd  18641  gsumress  18645  ismgmhm  18659  resmgmhm  18674  issgrp  18683  sgrppropd  18694  ismnddef  18699  ismndd  18719  mndpropd  18722  ismhm  18745  resmhm  18780  isgrp  18904  grppropd  18916  isgrpd2e  18920  isnsg  19118  nmznsg  19131  isghm  19178  isghmOLD  19179  isga  19254  subgga  19263  gsmsymgrfix  19395  gsmsymgreq  19399  gexval  19545  ispgp  19559  isslw  19575  sylow2blem2  19588  efgval  19684  efgi  19686  efgsdm  19697  cmnpropd  19758  iscmnd  19761  submcmn2  19806  gsumzaddlem  19888  dmdprd  19967  dprdcntz  19977  isrng  20106  rngpropd  20126  issrg  20140  isring  20189  ringpropd  20236  isirred  20370  c0snmgmhm  20413  islring  20489  sdrgacs  20701  abvfval  20710  abvpropd  20734  islmod  20759  islmodd  20761  lmodprop2d  20819  lssset  20829  islmhm  20924  reslmhm  20949  lmhmpropd  20970  islbs  20973  rrgval  21251  isdomn  21258  psgndiflemA  21550  isphl  21577  islindf  21763  islindf2  21765  lsslindf  21781  isassa  21807  isassad  21815  assapropd  21822  ltbval  22003  opsrval  22006  dmatval  22438  dmatcrng  22448  scmatcrng  22467  cpmat  22655  istopg  22841  restbas  23106  ordtrest2  23152  cnfval  23181  cnpfval  23182  ist0  23268  ist1  23269  ishaus  23270  iscnrm  23271  isnrm  23283  ist0-2  23292  ishaus2  23299  nrmsep3  23303  iscmp  23336  is1stc  23389  isptfin  23464  islocfin  23465  kgenval  23483  kgencn2  23505  txbas  23515  ptval  23518  dfac14  23566  isfil  23795  isufil  23851  isufl  23861  flfcntr  23991  ucnval  24226  iscusp  24248  prdsxmslem2  24482  tngngp3  24617  isnlm  24636  nmofval  24675  lebnumii  24936  iscau4  25251  iscmet  25256  iscmet3lem1  25263  iscmet3  25265  equivcmet  25289  ulmcaulem  26375  ulmcau  26376  fsumdvdscom  27162  dchrisumlem3  27469  pntibndlem2  27569  pntibnd  27571  pntlemp  27588  ostth2lem2  27612  madebdayim  27860  no2indslem  27917  no3inds  27921  istrkgc  28330  istrkgb  28331  istrkge  28333  trgcgrg  28391  tgcgr4  28407  isismt  28410  nbgr2vtx1edg  29235  nbuhgr2vtx1edgb  29237  uvtxval  29272  uvtxel  29273  uvtxel1  29281  uvtxusgrel  29288  cusgredg  29309  cplgr3v  29320  cplgrop  29322  usgredgsscusgredg  29345  isrgr  29445  isewlk  29488  iswlk  29496  iswwlks  29719  wlkiswwlks2  29758  isclwwlk  29866  clwlkclwwlklem1  29881  isconngr  30071  isconngr1  30072  isfrgr  30142  frgr1v  30153  nfrgr2v  30154  frgr3v  30157  1vwmgr  30158  3vfriswmgr  30160  3cyclfrgrrn1  30167  n4cyclfrgr  30173  isplig  30358  gidval  30394  vciOLD  30443  isvclem  30459  isnvlem  30492  lnoval  30634  ajfval  30691  isphg  30699  minvecolem3  30758  htth  30800  ressprs  32779  mntoval  32798  mgcoval  32802  isslmd  33001  resv1r  33152  prmidlval  33249  mxidlval  33273  rprmval  33328  isufd  33352  iscref  33573  ordtrest2NEW  33652  fmcncfil  33660  issiga  33859  isrnsiga  33860  isldsys  33903  ismeas  33946  carsgval  34051  issibf  34081  sitgfval  34089  signstfvneq0  34332  istrkg2d  34426  ispconn  34961  issconn  34964  txpconn  34970  cvxpconn  34980  cvmscbv  34996  iscvm  34997  cvmsdisj  35008  cvmsss2  35012  snmlval  35069  elmrsubrn  35258  ismfs  35287  mclsval  35301  fwddifnval  35887  bj-ismoore  36712  pibp19  37021  pibp21  37022  poimirlem28  37249  cover2g  37317  seqpo  37348  incsequz2  37350  caushft  37362  ismtyval  37401  isass  37447  isexid  37448  elghomlem1OLD  37486  isrngo  37498  isrngod  37499  isgrpda  37556  rngohomval  37565  iscom2  37596  idlval  37614  pridlval  37634  maxidlval  37640  elrefrels3  38118  elcnvrefrels3  38134  eleqvrels3  38192  lflset  38658  islfld  38661  isopos  38779  isoml  38837  isatl  38898  iscvlat  38922  ishlat1  38951  psubspset  39344  lautset  39682  pautsetN  39698  ldilfset  39708  ltrnfset  39717  dilfsetN  39752  trnfsetN  39755  trnsetN  39756  trlfset  39760  tendofset  40358  tendoset  40359  dihffval  40830  lpolsetN  41082  hdmapfval  41427  hgmapfval  41486  sn-isghm  42229  aomclem8  42624  islnm  42640  clsk1independent  43615  gneispace2  43701  gneispaceel2  43713  gneispacess2  43715  caucvgbf  45007  ioodvbdlimc1lem1  45454  ioodvbdlimc1lem2  45455  ioodvbdlimc2lem  45457  issal  45837  ismea  45974  isome  46017  iccpartiltu  46896  iccelpart  46907  isgrim  47349  isupwlk  47381  iscllaw  47434  iscomlaw  47435  isasslaw  47437  zlidlring  47479  uzlidlring  47480  dmatALTval  47651  islininds  47697  lindslinindsimp2  47714  ldepsnlinc  47759  elbigo  47807  iscnrm3r  48150  isprsd  48157  lubeldm2d  48160  glbeldm2d  48161  isthincd2lem2  48225  isthincd  48226