Theorem raleqbidv 3337

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  rspc2vd  3884  frd  5549  f12dfv  7154  f13dfv  7155  knatar  7237  ofrfvalg  7550  fmpox  7916  ovmptss  7942  frrlem4  8114  marypha1lem  9201  supeq123d  9218  oieq1  9280  acneq  9808  isfin1a  10057  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwecbv  10409  fpwwelem  10410  eltskg  10515  elgrug  10557  cau3lem  15075  rlim  15213  ello1  15233  elo1  15244  caurcvg2  15398  caucvgb  15400  fsum2dlem  15491  fsumcom2  15495  fprod2dlem  15699  fprodcom2  15703  pcfac  16609  vdwpc  16690  rami  16725  prmgaplem7  16767  prdsval  17175  ismre  17308  isacs2  17371  acsfiel  17372  iscat  17390  iscatd  17391  catidex  17392  catideu  17393  cidfval  17394  cidval  17395  catlid  17401  catrid  17402  comfeq  17424  catpropd  17427  monfval  17453  issubc  17559  fullsubc  17574  isfunc  17588  funcpropd  17625  isfull  17635  isfth  17639  fthpropd  17646  natfval  17671  initoval  17717  termoval  17718  isposd  18050  lubfval  18077  glbfval  18090  ismgm  18336  issstrmgm  18346  grpidval  18354  gsumvalx  18369  gsumpropd  18371  gsumress  18375  issgrp  18385  ismnddef  18396  ismndd  18416  mndpropd  18419  ismhm  18441  resmhm  18468  isgrp  18592  grppropd  18603  isgrpd2e  18607  isnsg  18792  nmznsg  18805  isghm  18843  isga  18906  subgga  18915  gsmsymgrfix  19045  gsmsymgreq  19049  gexval  19192  ispgp  19206  isslw  19222  sylow2blem2  19235  efgval  19332  efgi  19334  efgsdm  19345  cmnpropd  19405  iscmnd  19408  submcmn2  19449  gsumzaddlem  19531  dmdprd  19610  dprdcntz  19620  issrg  19752  isring  19796  ringpropd  19830  isirred  19950  sdrgacs  20078  abvfval  20087  abvpropd  20111  islmod  20136  islmodd  20138  lmodprop2d  20194  lssset  20204  islmhm  20298  reslmhm  20323  lmhmpropd  20344  islbs  20347  rrgval  20567  isdomn  20574  psgndiflemA  20815  isphl  20842  islindf  21028  islindf2  21030  lsslindf  21046  isassa  21072  isassad  21080  assapropd  21085  ltbval  21253  opsrval  21256  dmatval  21650  dmatcrng  21660  scmatcrng  21679  cpmat  21867  istopg  22053  restbas  22318  ordtrest2  22364  cnfval  22393  cnpfval  22394  ist0  22480  ist1  22481  ishaus  22482  iscnrm  22483  isnrm  22495  ist0-2  22504  ishaus2  22511  nrmsep3  22515  iscmp  22548  is1stc  22601  isptfin  22676  islocfin  22677  kgenval  22695  kgencn2  22717  txbas  22727  ptval  22730  dfac14  22778  isfil  23007  isufil  23063  isufl  23073  flfcntr  23203  ucnval  23438  iscusp  23460  prdsxmslem2  23694  tngngp3  23829  isnlm  23848  nmofval  23887  lebnumii  24138  iscau4  24452  iscmet  24457  iscmet3lem1  24464  iscmet3  24466  equivcmet  24490  ulmcaulem  25562  ulmcau  25563  fsumdvdscom  26343  dchrisumlem3  26648  pntibndlem2  26748  pntibnd  26750  pntlemp  26767  ostth2lem2  26791  trgcgrg  26885  tgcgr4  26901  isismt  26904  nbgr2vtx1edg  27726  nbuhgr2vtx1edgb  27728  uvtxval  27763  uvtxel  27764  uvtxel1  27772  uvtxusgrel  27779  cusgredg  27800  cplgr3v  27811  cplgrop  27813  usgredgsscusgredg  27835  isrgr  27935  isewlk  27978  iswlk  27986  iswwlks  28210  wlkiswwlks2  28249  isclwwlk  28357  clwlkclwwlklem1  28372  isconngr  28562  isconngr1  28563  isfrgr  28633  frgr1v  28644  nfrgr2v  28645  frgr3v  28648  1vwmgr  28649  3vfriswmgr  28651  3cyclfrgrrn1  28658  n4cyclfrgr  28664  isplig  28847  gidval  28883  vciOLD  28932  isvclem  28948  isnvlem  28981  lnoval  29123  ajfval  29180  isphg  29188  minvecolem3  29247  htth  29289  ressprs  31250  mntoval  31269  mgcoval  31273  isslmd  31464  resv1r  31550  prmidlval  31621  mxidlval  31642  isufd  31672  rprmval  31673  iscref  31803  ordtrest2NEW  31882  fmcncfil  31890  issiga  32089  isrnsiga  32090  isldsys  32133  ismeas  32176  carsgval  32279  issibf  32309  sitgfval  32317  signstfvneq0  32560  istrkg2d  32655  ispconn  33194  issconn  33197  txpconn  33203  cvxpconn  33213  cvmscbv  33229  iscvm  33230  cvmsdisj  33241  cvmsss2  33245  snmlval  33302  elmrsubrn  33491  ismfs  33520  mclsval  33534  on2ind  33837  on3ind  33838  madebdayim  34079  no2indslem  34120  no3inds  34124  fwddifnval  34474  bj-ismoore  35285  pibp19  35594  pibp21  35595  poimirlem28  35814  cover2g  35882  seqpo  35914  incsequz2  35916  caushft  35928  ismtyval  35967  isass  36013  isexid  36014  elghomlem1OLD  36052  isrngo  36064  isrngod  36065  isgrpda  36122  rngohomval  36131  iscom2  36162  idlval  36180  pridlval  36200  maxidlval  36206  elrefrels3  36643  elcnvrefrels3  36656  eleqvrels3  36713  lflset  37080  islfld  37083  isopos  37201  isoml  37259  isatl  37320  iscvlat  37344  ishlat1  37373  psubspset  37765  lautset  38103  pautsetN  38119  ldilfset  38129  ltrnfset  38138  dilfsetN  38173  trnfsetN  38176  trnsetN  38177  trlfset  38181  tendofset  38779  tendoset  38780  dihffval  39251  lpolsetN  39503  hdmapfval  39848  hgmapfval  39907  aomclem8  40893  islnm  40909  clsk1independent  41663  gneispace2  41749  gneispaceel2  41761  gneispacess2  41763  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  issal  43862  ismea  43996  isome  44039  iccpartiltu  44885  iccelpart  44896  isomgr  45286  isupwlk  45309  mgmpropd  45340  ismgmd  45341  ismgmhm  45348  resmgmhm  45363  iscllaw  45394  iscomlaw  45395  isasslaw  45397  isrng  45445  c0snmgmhm  45483  zlidlring  45497  uzlidlring  45498  dmatALTval  45752  islininds  45798  lindslinindsimp2  45815  ldepsnlinc  45860  elbigo  45908  iscnrm3r  46253  isprsd  46260  lubeldm2d  46263  glbeldm2d  46264  isthincd2lem2  46328  isthincd  46329