Theorem raleqbidv 3316

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspc2vd  3907  frd  5588  f12dfv  7230  f13dfv  7231  knatar  7314  ofrfvalg  7641  fmpox  8025  ovmptss  8049  frrlem4  8245  on2ind  8610  on3ind  8611  marypha1lem  9360  supeq123d  9377  oieq1  9441  acneq  9972  isfin1a  10221  fpwwe2cbv  10559  fpwwe2lem2  10561  fpwwecbv  10573  fpwwelem  10574  eltskg  10679  elgrug  10721  cau3lem  15297  rlim  15437  ello1  15457  elo1  15468  caurcvg2  15620  caucvgb  15622  fsum2dlem  15712  fsumcom2  15716  fprod2dlem  15922  fprodcom2  15926  pcfac  16846  vdwpc  16927  rami  16962  prmgaplem7  17004  prdsval  17394  ismre  17527  isacs2  17594  acsfiel  17595  iscat  17613  iscatd  17614  catidex  17615  catideu  17616  cidfval  17617  cidval  17618  catlid  17624  catrid  17625  comfeq  17647  catpropd  17650  monfval  17674  issubc  17777  fullsubc  17792  isfunc  17806  funcpropd  17844  isfull  17854  isfth  17858  fthpropd  17865  natfval  17891  initoval  17935  termoval  17936  isposd  18263  lubfval  18289  glbfval  18302  ismgm  18550  mgmpropd  18560  ismgmd  18561  issstrmgm  18562  grpidval  18570  gsumvalx  18585  gsumpropd  18587  gsumress  18591  ismgmhm  18605  resmgmhm  18620  issgrp  18629  sgrppropd  18640  ismnddef  18645  ismndd  18665  mndpropd  18668  ismhm  18694  resmhm  18729  isgrp  18853  grppropd  18865  isgrpd2e  18869  isnsg  19069  nmznsg  19082  isghm  19129  isghmOLD  19130  isga  19205  subgga  19214  gsmsymgrfix  19342  gsmsymgreq  19346  gexval  19492  ispgp  19506  isslw  19522  sylow2blem2  19535  efgval  19631  efgi  19633  efgsdm  19644  cmnpropd  19705  iscmnd  19708  submcmn2  19753  gsumzaddlem  19835  dmdprd  19914  dprdcntz  19924  isrng  20074  rngpropd  20094  issrg  20108  isring  20157  ringpropd  20208  isirred  20339  c0snmgmhm  20382  islring  20460  rrgval  20617  isdomn  20625  sdrgacs  20721  abvfval  20730  abvpropd  20755  islmod  20802  islmodd  20804  lmodprop2d  20862  lssset  20871  islmhm  20966  reslmhm  20991  lmhmpropd  21012  islbs  21015  psgndiflemA  21543  isphl  21570  islindf  21754  islindf2  21756  lsslindf  21772  isassa  21798  isassad  21807  assapropd  21814  ltbval  21983  opsrval  21986  dmatval  22412  dmatcrng  22422  scmatcrng  22441  cpmat  22629  istopg  22815  restbas  23078  ordtrest2  23124  cnfval  23153  cnpfval  23154  ist0  23240  ist1  23241  ishaus  23242  iscnrm  23243  isnrm  23255  ist0-2  23264  ishaus2  23271  nrmsep3  23275  iscmp  23308  is1stc  23361  isptfin  23436  islocfin  23437  kgenval  23455  kgencn2  23477  txbas  23487  ptval  23490  dfac14  23538  isfil  23767  isufil  23823  isufl  23833  flfcntr  23963  ucnval  24197  iscusp  24219  prdsxmslem2  24450  tngngp3  24577  isnlm  24596  nmofval  24635  lebnumii  24898  iscau4  25212  iscmet  25217  iscmet3lem1  25224  iscmet3  25226  equivcmet  25250  ulmcaulem  26336  ulmcau  26337  fsumdvdscom  27128  dchrisumlem3  27435  pntibndlem2  27535  pntibnd  27537  pntlemp  27554  ostth2lem2  27578  madebdayim  27837  no2indslem  27901  no3inds  27905  istrkgc  28434  istrkgb  28435  istrkge  28437  trgcgrg  28495  tgcgr4  28511  isismt  28514  nbgr2vtx1edg  29330  nbuhgr2vtx1edgb  29332  uvtxval  29367  uvtxel  29368  uvtxel1  29376  uvtxusgrel  29383  cusgredg  29404  cplgr3v  29415  cplgrop  29417  usgredgsscusgredg  29440  isrgr  29540  isewlk  29583  iswlk  29591  iswwlks  29816  wlkiswwlks2  29855  isclwwlk  29963  clwlkclwwlklem1  29978  isconngr  30168  isconngr1  30169  isfrgr  30239  frgr1v  30250  nfrgr2v  30251  frgr3v  30254  1vwmgr  30255  3vfriswmgr  30257  3cyclfrgrrn1  30264  n4cyclfrgr  30270  isplig  30455  gidval  30491  vciOLD  30540  isvclem  30556  isnvlem  30589  lnoval  30731  ajfval  30788  isphg  30796  minvecolem3  30855  htth  30897  ressprs  32938  mntoval  32954  mgcoval  32958  ischn  32978  chnind  32983  chnub  32984  fxpval  33137  isslmd  33171  resv1r  33304  prmidlval  33401  mxidlval  33425  rprmval  33480  isufd  33504  constrconj  33728  iscref  33827  ordtrest2NEW  33906  fmcncfil  33914  issiga  34095  isrnsiga  34096  isldsys  34139  ismeas  34182  carsgval  34287  issibf  34317  sitgfval  34325  signstfvneq0  34556  istrkg2d  34650  ispconn  35203  issconn  35206  txpconn  35212  cvxpconn  35222  cvmscbv  35238  iscvm  35239  cvmsdisj  35250  cvmsss2  35254  snmlval  35311  elmrsubrn  35500  ismfs  35529  mclsval  35543  fwddifnval  36144  weiunfrlem  36445  bj-ismoore  37086  pibp19  37395  pibp21  37396  poimirlem28  37635  cover2g  37703  seqpo  37734  incsequz2  37736  caushft  37748  ismtyval  37787  isass  37833  isexid  37834  elghomlem1OLD  37872  isrngo  37884  isrngod  37885  isgrpda  37942  rngohomval  37951  iscom2  37982  idlval  38000  pridlval  38020  maxidlval  38026  elrefrels3  38503  elcnvrefrels3  38519  eleqvrels3  38577  lflset  39045  islfld  39048  isopos  39166  isoml  39224  isatl  39285  iscvlat  39309  ishlat1  39338  psubspset  39731  lautset  40069  pautsetN  40085  ldilfset  40095  ltrnfset  40104  dilfsetN  40139  trnfsetN  40142  trnsetN  40143  trlfset  40147  tendofset  40745  tendoset  40746  dihffval  41217  lpolsetN  41469  hdmapfval  41814  hgmapfval  41873  sn-isghm  42654  aomclem8  43043  islnm  43059  clsk1independent  44028  gneispace2  44114  gneispaceel2  44126  gneispacess2  44128  caucvgbf  45478  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  issal  46305  ismea  46442  isome  46485  iccpartiltu  47416  iccelpart  47427  isgrim  47875  isubgrgrim  47922  isgrlim  47974  usgrexmpl2trifr  48021  gpg5nbgr3star  48065  isupwlk  48117  iscllaw  48170  iscomlaw  48171  isasslaw  48173  zlidlring  48215  uzlidlring  48216  dmatALTval  48382  islininds  48428  lindslinindsimp2  48445  ldepsnlinc  48490  elbigo  48533  iscnrm3r  48929  isprsd  48936  lubeldm2d  48939  glbeldm2d  48940  nelsubc3lem  49052  ssccatid  49054  resccatlem  49055  upciclem1  49148  upfval  49158  upfval2  49159  upfval3  49160  oppcup3lem  49188  oppcup  49189  uptr2  49203  isthincd2lem2  49417  isthincd  49418  thincpropd  49424