Theorem raleqbidv 3346

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2141, ax-11 2157, and ax-12 2177 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 2827	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	imbi12d 344	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))
5	4	ralbidv2 3174	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-ral 3062

This theorem is referenced by:  rspc2vd  3947  frd  5641  f12dfv  7293  f13dfv  7294  knatar  7377  ofrfvalg  7705  fmpox  8092  ovmptss  8118  frrlem4  8314  on2ind  8707  on3ind  8708  marypha1lem  9473  supeq123d  9490  oieq1  9552  acneq  10083  isfin1a  10332  fpwwe2cbv  10670  fpwwe2lem2  10672  fpwwecbv  10684  fpwwelem  10685  eltskg  10790  elgrug  10832  cau3lem  15393  rlim  15531  ello1  15551  elo1  15562  caurcvg2  15714  caucvgb  15716  fsum2dlem  15806  fsumcom2  15810  fprod2dlem  16016  fprodcom2  16020  pcfac  16937  vdwpc  17018  rami  17053  prmgaplem7  17095  prdsval  17500  ismre  17633  isacs2  17696  acsfiel  17697  iscat  17715  iscatd  17716  catidex  17717  catideu  17718  cidfval  17719  cidval  17720  catlid  17726  catrid  17727  comfeq  17749  catpropd  17752  monfval  17776  issubc  17880  fullsubc  17895  isfunc  17909  funcpropd  17947  isfull  17957  isfth  17961  fthpropd  17968  natfval  17994  initoval  18038  termoval  18039  isposd  18368  lubfval  18395  glbfval  18408  ismgm  18654  mgmpropd  18664  ismgmd  18665  issstrmgm  18666  grpidval  18674  gsumvalx  18689  gsumpropd  18691  gsumress  18695  ismgmhm  18709  resmgmhm  18724  issgrp  18733  sgrppropd  18744  ismnddef  18749  ismndd  18769  mndpropd  18772  ismhm  18798  resmhm  18833  isgrp  18957  grppropd  18969  isgrpd2e  18973  isnsg  19173  nmznsg  19186  isghm  19233  isghmOLD  19234  isga  19309  subgga  19318  gsmsymgrfix  19446  gsmsymgreq  19450  gexval  19596  ispgp  19610  isslw  19626  sylow2blem2  19639  efgval  19735  efgi  19737  efgsdm  19748  cmnpropd  19809  iscmnd  19812  submcmn2  19857  gsumzaddlem  19939  dmdprd  20018  dprdcntz  20028  isrng  20151  rngpropd  20171  issrg  20185  isring  20234  ringpropd  20285  isirred  20419  c0snmgmhm  20462  islring  20540  rrgval  20697  isdomn  20705  sdrgacs  20802  abvfval  20811  abvpropd  20836  islmod  20862  islmodd  20864  lmodprop2d  20922  lssset  20931  islmhm  21026  reslmhm  21051  lmhmpropd  21072  islbs  21075  psgndiflemA  21619  isphl  21646  islindf  21832  islindf2  21834  lsslindf  21850  isassa  21876  isassad  21885  assapropd  21892  ltbval  22061  opsrval  22064  dmatval  22498  dmatcrng  22508  scmatcrng  22527  cpmat  22715  istopg  22901  restbas  23166  ordtrest2  23212  cnfval  23241  cnpfval  23242  ist0  23328  ist1  23329  ishaus  23330  iscnrm  23331  isnrm  23343  ist0-2  23352  ishaus2  23359  nrmsep3  23363  iscmp  23396  is1stc  23449  isptfin  23524  islocfin  23525  kgenval  23543  kgencn2  23565  txbas  23575  ptval  23578  dfac14  23626  isfil  23855  isufil  23911  isufl  23921  flfcntr  24051  ucnval  24286  iscusp  24308  prdsxmslem2  24542  tngngp3  24677  isnlm  24696  nmofval  24735  lebnumii  24998  iscau4  25313  iscmet  25318  iscmet3lem1  25325  iscmet3  25327  equivcmet  25351  ulmcaulem  26437  ulmcau  26438  fsumdvdscom  27228  dchrisumlem3  27535  pntibndlem2  27635  pntibnd  27637  pntlemp  27654  ostth2lem2  27678  madebdayim  27926  no2indslem  27987  no3inds  27991  istrkgc  28462  istrkgb  28463  istrkge  28465  trgcgrg  28523  tgcgr4  28539  isismt  28542  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  uvtxval  29404  uvtxel  29405  uvtxel1  29413  uvtxusgrel  29420  cusgredg  29441  cplgr3v  29452  cplgrop  29454  usgredgsscusgredg  29477  isrgr  29577  isewlk  29620  iswlk  29628  iswwlks  29856  wlkiswwlks2  29895  isclwwlk  30003  clwlkclwwlklem1  30018  isconngr  30208  isconngr1  30209  isfrgr  30279  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  1vwmgr  30295  3vfriswmgr  30297  3cyclfrgrrn1  30304  n4cyclfrgr  30310  isplig  30495  gidval  30531  vciOLD  30580  isvclem  30596  isnvlem  30629  lnoval  30771  ajfval  30828  isphg  30836  minvecolem3  30895  htth  30937  ressprs  32954  mntoval  32972  mgcoval  32976  ischn  32996  chnind  33001  chnub  33002  isslmd  33208  resv1r  33368  prmidlval  33465  mxidlval  33489  rprmval  33544  isufd  33568  constrconj  33786  iscref  33843  ordtrest2NEW  33922  fmcncfil  33930  issiga  34113  isrnsiga  34114  isldsys  34157  ismeas  34200  carsgval  34305  issibf  34335  sitgfval  34343  signstfvneq0  34587  istrkg2d  34681  ispconn  35228  issconn  35231  txpconn  35237  cvxpconn  35247  cvmscbv  35263  iscvm  35264  cvmsdisj  35275  cvmsss2  35279  snmlval  35336  elmrsubrn  35525  ismfs  35554  mclsval  35568  fwddifnval  36164  weiunfrlem  36465  bj-ismoore  37106  pibp19  37415  pibp21  37416  poimirlem28  37655  cover2g  37723  seqpo  37754  incsequz2  37756  caushft  37768  ismtyval  37807  isass  37853  isexid  37854  elghomlem1OLD  37892  isrngo  37904  isrngod  37905  isgrpda  37962  rngohomval  37971  iscom2  38002  idlval  38020  pridlval  38040  maxidlval  38046  elrefrels3  38520  elcnvrefrels3  38536  eleqvrels3  38594  lflset  39060  islfld  39063  isopos  39181  isoml  39239  isatl  39300  iscvlat  39324  ishlat1  39353  psubspset  39746  lautset  40084  pautsetN  40100  ldilfset  40110  ltrnfset  40119  dilfsetN  40154  trnfsetN  40157  trnsetN  40158  trlfset  40162  tendofset  40760  tendoset  40761  dihffval  41232  lpolsetN  41484  hdmapfval  41829  hgmapfval  41888  sn-isghm  42683  aomclem8  43073  islnm  43089  clsk1independent  44059  gneispace2  44145  gneispaceel2  44157  gneispacess2  44159  caucvgbf  45500  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  issal  46329  ismea  46466  isome  46509  iccpartiltu  47409  iccelpart  47420  isgrim  47868  isubgrgrim  47897  isgrlim  47949  usgrexmpl2trifr  47996  gpg5nbgr3star  48037  isupwlk  48052  iscllaw  48105  iscomlaw  48106  isasslaw  48108  zlidlring  48150  uzlidlring  48151  dmatALTval  48317  islininds  48363  lindslinindsimp2  48380  ldepsnlinc  48425  elbigo  48472  iscnrm3r  48845  isprsd  48852  lubeldm2d  48855  glbeldm2d  48856  upciclem1  48923  upfval  48933  upfval2  48934  upfval3  48935  oppcup  48948  isthincd2lem2  49084  isthincd  49085  thincpropd  49091