Theorem raleqbidv 3343

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 2820	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	imbi12d 345	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))
5	4	ralbidv2 3174	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

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

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  rspc2vd  3945  frd  5636  f12dfv  7271  f13dfv  7272  knatar  7354  ofrfvalg  7678  fmpox  8053  ovmptss  8079  frrlem4  8274  on2ind  8668  on3ind  8669  marypha1lem  9428  supeq123d  9445  oieq1  9507  acneq  10038  isfin1a  10287  fpwwe2cbv  10625  fpwwe2lem2  10627  fpwwecbv  10639  fpwwelem  10640  eltskg  10745  elgrug  10787  cau3lem  15301  rlim  15439  ello1  15459  elo1  15470  caurcvg2  15624  caucvgb  15626  fsum2dlem  15716  fsumcom2  15720  fprod2dlem  15924  fprodcom2  15928  pcfac  16832  vdwpc  16913  rami  16948  prmgaplem7  16990  prdsval  17401  ismre  17534  isacs2  17597  acsfiel  17598  iscat  17616  iscatd  17617  catidex  17618  catideu  17619  cidfval  17620  cidval  17621  catlid  17627  catrid  17628  comfeq  17650  catpropd  17653  monfval  17679  issubc  17785  fullsubc  17800  isfunc  17814  funcpropd  17851  isfull  17861  isfth  17865  fthpropd  17872  natfval  17897  initoval  17943  termoval  17944  isposd  18276  lubfval  18303  glbfval  18316  ismgm  18562  issstrmgm  18572  grpidval  18580  gsumvalx  18595  gsumpropd  18597  gsumress  18601  issgrp  18611  sgrppropd  18622  ismnddef  18627  ismndd  18647  mndpropd  18650  ismhm  18673  resmhm  18701  isgrp  18825  grppropd  18837  isgrpd2e  18841  isnsg  19035  nmznsg  19048  isghm  19092  isga  19155  subgga  19164  gsmsymgrfix  19296  gsmsymgreq  19300  gexval  19446  ispgp  19460  isslw  19476  sylow2blem2  19489  efgval  19585  efgi  19587  efgsdm  19598  cmnpropd  19659  iscmnd  19662  submcmn2  19707  gsumzaddlem  19789  dmdprd  19868  dprdcntz  19878  issrg  20011  isring  20060  ringpropd  20102  isirred  20233  islring  20310  sdrgacs  20417  abvfval  20426  abvpropd  20450  islmod  20475  islmodd  20477  lmodprop2d  20534  lssset  20544  islmhm  20638  reslmhm  20663  lmhmpropd  20684  islbs  20687  rrgval  20903  isdomn  20910  psgndiflemA  21154  isphl  21181  islindf  21367  islindf2  21369  lsslindf  21385  isassa  21411  isassad  21419  assapropd  21426  ltbval  21598  opsrval  21601  dmatval  21994  dmatcrng  22004  scmatcrng  22023  cpmat  22211  istopg  22397  restbas  22662  ordtrest2  22708  cnfval  22737  cnpfval  22738  ist0  22824  ist1  22825  ishaus  22826  iscnrm  22827  isnrm  22839  ist0-2  22848  ishaus2  22855  nrmsep3  22859  iscmp  22892  is1stc  22945  isptfin  23020  islocfin  23021  kgenval  23039  kgencn2  23061  txbas  23071  ptval  23074  dfac14  23122  isfil  23351  isufil  23407  isufl  23417  flfcntr  23547  ucnval  23782  iscusp  23804  prdsxmslem2  24038  tngngp3  24173  isnlm  24192  nmofval  24231  lebnumii  24482  iscau4  24796  iscmet  24801  iscmet3lem1  24808  iscmet3  24810  equivcmet  24834  ulmcaulem  25906  ulmcau  25907  fsumdvdscom  26689  dchrisumlem3  26994  pntibndlem2  27094  pntibnd  27096  pntlemp  27113  ostth2lem2  27137  madebdayim  27382  no2indslem  27438  no3inds  27442  istrkgc  27705  istrkgb  27706  istrkge  27708  trgcgrg  27766  tgcgr4  27782  isismt  27785  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  uvtxval  28644  uvtxel  28645  uvtxel1  28653  uvtxusgrel  28660  cusgredg  28681  cplgr3v  28692  cplgrop  28694  usgredgsscusgredg  28716  isrgr  28816  isewlk  28859  iswlk  28867  iswwlks  29090  wlkiswwlks2  29129  isclwwlk  29237  clwlkclwwlklem1  29252  isconngr  29442  isconngr1  29443  isfrgr  29513  frgr1v  29524  nfrgr2v  29525  frgr3v  29528  1vwmgr  29529  3vfriswmgr  29531  3cyclfrgrrn1  29538  n4cyclfrgr  29544  isplig  29729  gidval  29765  vciOLD  29814  isvclem  29830  isnvlem  29863  lnoval  30005  ajfval  30062  isphg  30070  minvecolem3  30129  htth  30171  ressprs  32133  mntoval  32152  mgcoval  32156  isslmd  32347  resv1r  32456  prmidlval  32555  mxidlval  32577  isufd  32632  rprmval  32633  iscref  32824  ordtrest2NEW  32903  fmcncfil  32911  issiga  33110  isrnsiga  33111  isldsys  33154  ismeas  33197  carsgval  33302  issibf  33332  sitgfval  33340  signstfvneq0  33583  istrkg2d  33678  ispconn  34214  issconn  34217  txpconn  34223  cvxpconn  34233  cvmscbv  34249  iscvm  34250  cvmsdisj  34261  cvmsss2  34265  snmlval  34322  elmrsubrn  34511  ismfs  34540  mclsval  34554  fwddifnval  35135  bj-ismoore  35986  pibp19  36295  pibp21  36296  poimirlem28  36516  cover2g  36584  seqpo  36615  incsequz2  36617  caushft  36629  ismtyval  36668  isass  36714  isexid  36715  elghomlem1OLD  36753  isrngo  36765  isrngod  36766  isgrpda  36823  rngohomval  36832  iscom2  36863  idlval  36881  pridlval  36901  maxidlval  36907  elrefrels3  37389  elcnvrefrels3  37405  eleqvrels3  37463  lflset  37929  islfld  37932  isopos  38050  isoml  38108  isatl  38169  iscvlat  38193  ishlat1  38222  psubspset  38615  lautset  38953  pautsetN  38969  ldilfset  38979  ltrnfset  38988  dilfsetN  39023  trnfsetN  39026  trnsetN  39027  trlfset  39031  tendofset  39629  tendoset  39630  dihffval  40101  lpolsetN  40353  hdmapfval  40698  hgmapfval  40757  aomclem8  41803  islnm  41819  clsk1independent  42797  gneispace2  42883  gneispaceel2  42895  gneispacess2  42897  caucvgbf  44200  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  issal  45030  ismea  45167  isome  45210  iccpartiltu  46090  iccelpart  46101  isomgr  46491  isupwlk  46514  mgmpropd  46545  ismgmd  46546  ismgmhm  46553  resmgmhm  46568  iscllaw  46599  iscomlaw  46600  isasslaw  46602  isrng  46650  rngpropd  46673  c0snmgmhm  46713  zlidlring  46826  uzlidlring  46827  dmatALTval  47081  islininds  47127  lindslinindsimp2  47144  ldepsnlinc  47189  elbigo  47237  iscnrm3r  47581  isprsd  47588  lubeldm2d  47591  glbeldm2d  47592  isthincd2lem2  47656  isthincd  47657