Theorem raleqbidv 3341

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ 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  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771  df-clel 2846  df-ral 3093

This theorem is referenced by:  raleqbi1dv  3343  f12dfv  6857  f13dfv  6858  knatar  6935  ofrfval  7237  fmpox  7575  ovmptss  7598  marypha1lem  8694  supeq123d  8711  oieq1  8773  acneq  9265  isfin1a  9514  fpwwe2cbv  9852  fpwwe2lem2  9854  fpwwecbv  9866  fpwwelem  9867  eltskg  9972  elgrug  10014  cau3lem  14578  rlim  14716  ello1  14736  elo1  14747  caurcvg2  14898  caucvgb  14900  fsum2dlem  14988  fsumcom2  14992  fprod2dlem  15197  fprodcom2  15201  pcfac  16094  vdwpc  16175  rami  16210  prmgaplem7  16252  prdsval  16587  ismre  16722  isacs2  16785  acsfiel  16786  iscat  16804  iscatd  16805  catidex  16806  catideu  16807  cidfval  16808  cidval  16809  catlid  16815  catrid  16816  comfeq  16837  catpropd  16840  monfval  16863  issubc  16966  fullsubc  16981  isfunc  16995  funcpropd  17031  isfull  17041  isfth  17045  fthpropd  17052  natfval  17077  initoval  17118  termoval  17119  isposd  17426  lubfval  17449  glbfval  17462  ismgm  17714  issstrmgm  17723  grpidval  17731  gsumvalx  17741  gsumpropd  17743  gsumress  17747  issgrp  17756  ismnddef  17767  ismndd  17784  mndpropd  17787  ismhm  17808  resmhm  17830  isgrp  17900  grppropd  17909  isgrpd2e  17913  isnsg  18095  nmznsg  18110  isghm  18132  isga  18195  subgga  18204  gsmsymgrfix  18320  gsmsymgreq  18324  gexval  18467  ispgp  18481  isslw  18497  sylow2blem2  18510  efgval  18604  efgi  18606  efgsdm  18617  cmnpropd  18678  iscmnd  18681  submcmn2  18720  gsumzaddlem  18797  dmdprd  18873  dprdcntz  18883  issrg  18983  isring  19027  ringpropd  19058  isirred  19175  sdrgacs  19305  abvfval  19314  abvpropd  19338  islmod  19363  islmodd  19365  lmodprop2d  19421  lssset  19430  islmhm  19524  reslmhm  19549  lmhmpropd  19570  islbs  19573  rrgval  19784  isdomn  19791  isassa  19812  isassad  19820  assapropd  19824  ltbval  19968  opsrval  19971  psgndiflemA  20450  isphl  20477  islindf  20661  islindf2  20663  lsslindf  20679  dmatval  20808  dmatcrng  20818  scmatcrng  20837  cpmat  21024  istopg  21210  restbas  21473  ordtrest2  21519  cnfval  21548  cnpfval  21549  ist0  21635  ist1  21636  ishaus  21637  iscnrm  21638  isnrm  21650  ist0-2  21659  ishaus2  21666  nrmsep3  21670  iscmp  21703  is1stc  21756  isptfin  21831  islocfin  21832  kgenval  21850  kgencn2  21872  txbas  21882  ptval  21885  dfac14  21933  isfil  22162  isufil  22218  isufl  22228  flfcntr  22358  ucnval  22592  iscusp  22614  prdsxmslem2  22845  tngngp3  22971  isnlm  22990  nmofval  23029  lebnumii  23276  iscau4  23588  iscmet  23593  iscmet3lem1  23600  iscmet3  23602  equivcmet  23626  ulmcaulem  24688  ulmcau  24689  fsumdvdscom  25467  dchrisumlem3  25772  pntibndlem2  25872  pntibnd  25874  pntlemp  25891  ostth2lem2  25915  trgcgrg  26006  tgcgr4  26022  isismt  26025  nbgr2vtx1edg  26838  nbuhgr2vtx1edgb  26840  uvtxval  26875  uvtxel  26876  uvtxel1  26884  uvtxusgrel  26891  cusgredg  26912  cplgr3v  26923  cplgrop  26925  usgredgsscusgredg  26947  isrgr  27047  isewlk  27090  iswlk  27098  iswwlks  27325  wlkiswwlks2  27364  isclwwlk  27493  clwlkclwwlklem1  27508  isconngr  27721  isconngr1  27722  isfrgr  27795  rspc2vd  27802  frgr1v  27808  nfrgr2v  27809  frgr3v  27812  1vwmgr  27813  3vfriswmgr  27815  3cyclfrgrrn1  27822  n4cyclfrgr  27828  isplig  28033  gidval  28069  vciOLD  28118  isvclem  28134  isnvlem  28167  lnoval  28309  ajfval  28366  isphg  28374  minvecolem3  28434  htth  28477  ressprs  30374  isslmd  30496  resv1r  30589  iscref  30752  ordtrest2NEW  30810  fmcncfil  30818  issiga  31015  isrnsigaOLD  31016  isrnsiga  31017  isldsys  31060  ismeas  31103  carsgval  31206  issibf  31236  sitgfval  31244  signstfvneq0  31489  istrkg2d  31585  ispconn  32055  issconn  32058  txpconn  32064  cvxpconn  32074  cvmscbv  32090  iscvm  32091  cvmsdisj  32102  cvmsss2  32106  snmlval  32163  elmrsubrn  32287  ismfs  32316  mclsval  32330  frrlem4  32647  fwddifnval  33145  bj-ismoore  33907  pibp19  34136  pibp21  34137  poimirlem28  34361  cover2g  34432  seqpo  34464  incsequz2  34466  caushft  34478  ismtyval  34520  isass  34566  isexid  34567  elghomlem1OLD  34605  isrngo  34617  isrngod  34618  isgrpda  34675  rngohomval  34684  iscom2  34715  idlval  34733  pridlval  34753  maxidlval  34759  elrefrels3  35203  elcnvrefrels3  35216  eleqvrels3  35273  lflset  35640  islfld  35643  isopos  35761  isoml  35819  isatl  35880  iscvlat  35904  ishlat1  35933  psubspset  36325  lautset  36663  pautsetN  36679  ldilfset  36689  ltrnfset  36698  dilfsetN  36733  trnfsetN  36736  trnsetN  36737  trlfset  36741  tendofset  37339  tendoset  37340  dihffval  37811  lpolsetN  38063  hdmapfval  38408  hgmapfval  38467  aomclem8  39057  islnm  39073  clsk1independent  39759  gneispace2  39845  gneispaceel2  39857  gneispacess2  39859  ioodvbdlimc1lem1  41647  ioodvbdlimc1lem2  41648  ioodvbdlimc2lem  41650  issal  42031  ismea  42165  isome  42208  iccpartiltu  42955  iccelpart  42966  isomgr  43357  isupwlk  43380  mgmpropd  43411  ismgmd  43412  ismgmhm  43419  resmgmhm  43434  iscllaw  43461  iscomlaw  43462  isasslaw  43464  isrng  43512  c0snmgmhm  43550  zlidlring  43564  uzlidlring  43565  dmatALTval  43823  islininds  43869  lindslinindsimp2  43886  ldepsnlinc  43931  elbigo  43980