Theorem raleqbidv 3342

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  rspc2vd  3943  frd  5634  f12dfv  7267  f13dfv  7268  knatar  7350  ofrfvalg  7674  fmpox  8049  ovmptss  8075  frrlem4  8270  on2ind  8664  on3ind  8665  marypha1lem  9424  supeq123d  9441  oieq1  9503  acneq  10034  isfin1a  10283  fpwwe2cbv  10621  fpwwe2lem2  10623  fpwwecbv  10635  fpwwelem  10636  eltskg  10741  elgrug  10783  cau3lem  15297  rlim  15435  ello1  15455  elo1  15466  caurcvg2  15620  caucvgb  15622  fsum2dlem  15712  fsumcom2  15716  fprod2dlem  15920  fprodcom2  15924  pcfac  16828  vdwpc  16909  rami  16944  prmgaplem7  16986  prdsval  17397  ismre  17530  isacs2  17593  acsfiel  17594  iscat  17612  iscatd  17613  catidex  17614  catideu  17615  cidfval  17616  cidval  17617  catlid  17623  catrid  17624  comfeq  17646  catpropd  17649  monfval  17675  issubc  17781  fullsubc  17796  isfunc  17810  funcpropd  17847  isfull  17857  isfth  17861  fthpropd  17868  natfval  17893  initoval  17939  termoval  17940  isposd  18272  lubfval  18299  glbfval  18312  ismgm  18558  issstrmgm  18568  grpidval  18576  gsumvalx  18591  gsumpropd  18593  gsumress  18597  issgrp  18607  sgrppropd  18618  ismnddef  18623  ismndd  18643  mndpropd  18646  ismhm  18669  resmhm  18697  isgrp  18821  grppropd  18833  isgrpd2e  18837  isnsg  19029  nmznsg  19042  isghm  19086  isga  19149  subgga  19158  gsmsymgrfix  19290  gsmsymgreq  19294  gexval  19440  ispgp  19454  isslw  19470  sylow2blem2  19483  efgval  19579  efgi  19581  efgsdm  19592  cmnpropd  19653  iscmnd  19656  submcmn2  19701  gsumzaddlem  19783  dmdprd  19862  dprdcntz  19872  issrg  20004  isring  20053  ringpropd  20095  isirred  20225  islring  20302  sdrgacs  20409  abvfval  20418  abvpropd  20442  islmod  20467  islmodd  20469  lmodprop2d  20526  lssset  20536  islmhm  20630  reslmhm  20655  lmhmpropd  20676  islbs  20679  rrgval  20895  isdomn  20902  psgndiflemA  21145  isphl  21172  islindf  21358  islindf2  21360  lsslindf  21376  isassa  21402  isassad  21410  assapropd  21417  ltbval  21589  opsrval  21592  dmatval  21985  dmatcrng  21995  scmatcrng  22014  cpmat  22202  istopg  22388  restbas  22653  ordtrest2  22699  cnfval  22728  cnpfval  22729  ist0  22815  ist1  22816  ishaus  22817  iscnrm  22818  isnrm  22830  ist0-2  22839  ishaus2  22846  nrmsep3  22850  iscmp  22883  is1stc  22936  isptfin  23011  islocfin  23012  kgenval  23030  kgencn2  23052  txbas  23062  ptval  23065  dfac14  23113  isfil  23342  isufil  23398  isufl  23408  flfcntr  23538  ucnval  23773  iscusp  23795  prdsxmslem2  24029  tngngp3  24164  isnlm  24183  nmofval  24222  lebnumii  24473  iscau4  24787  iscmet  24792  iscmet3lem1  24799  iscmet3  24801  equivcmet  24825  ulmcaulem  25897  ulmcau  25898  fsumdvdscom  26678  dchrisumlem3  26983  pntibndlem2  27083  pntibnd  27085  pntlemp  27102  ostth2lem2  27126  madebdayim  27371  no2indslem  27427  no3inds  27431  istrkgc  27694  istrkgb  27695  istrkge  27697  trgcgrg  27755  tgcgr4  27771  isismt  27774  nbgr2vtx1edg  28596  nbuhgr2vtx1edgb  28598  uvtxval  28633  uvtxel  28634  uvtxel1  28642  uvtxusgrel  28649  cusgredg  28670  cplgr3v  28681  cplgrop  28683  usgredgsscusgredg  28705  isrgr  28805  isewlk  28848  iswlk  28856  iswwlks  29079  wlkiswwlks2  29118  isclwwlk  29226  clwlkclwwlklem1  29241  isconngr  29431  isconngr1  29432  isfrgr  29502  frgr1v  29513  nfrgr2v  29514  frgr3v  29517  1vwmgr  29518  3vfriswmgr  29520  3cyclfrgrrn1  29527  n4cyclfrgr  29533  isplig  29716  gidval  29752  vciOLD  29801  isvclem  29817  isnvlem  29850  lnoval  29992  ajfval  30049  isphg  30057  minvecolem3  30116  htth  30158  ressprs  32120  mntoval  32139  mgcoval  32143  isslmd  32334  resv1r  32444  prmidlval  32543  mxidlval  32565  isufd  32620  rprmval  32621  iscref  32812  ordtrest2NEW  32891  fmcncfil  32899  issiga  33098  isrnsiga  33099  isldsys  33142  ismeas  33185  carsgval  33290  issibf  33320  sitgfval  33328  signstfvneq0  33571  istrkg2d  33666  ispconn  34202  issconn  34205  txpconn  34211  cvxpconn  34221  cvmscbv  34237  iscvm  34238  cvmsdisj  34249  cvmsss2  34253  snmlval  34310  elmrsubrn  34499  ismfs  34528  mclsval  34542  fwddifnval  35123  bj-ismoore  35974  pibp19  36283  pibp21  36284  poimirlem28  36504  cover2g  36572  seqpo  36603  incsequz2  36605  caushft  36617  ismtyval  36656  isass  36702  isexid  36703  elghomlem1OLD  36741  isrngo  36753  isrngod  36754  isgrpda  36811  rngohomval  36820  iscom2  36851  idlval  36869  pridlval  36889  maxidlval  36895  elrefrels3  37377  elcnvrefrels3  37393  eleqvrels3  37451  lflset  37917  islfld  37920  isopos  38038  isoml  38096  isatl  38157  iscvlat  38181  ishlat1  38210  psubspset  38603  lautset  38941  pautsetN  38957  ldilfset  38967  ltrnfset  38976  dilfsetN  39011  trnfsetN  39014  trnsetN  39015  trlfset  39019  tendofset  39617  tendoset  39618  dihffval  40089  lpolsetN  40341  hdmapfval  40686  hgmapfval  40745  aomclem8  41788  islnm  41804  clsk1independent  42782  gneispace2  42868  gneispaceel2  42880  gneispacess2  42882  caucvgbf  44186  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  issal  45016  ismea  45153  isome  45196  iccpartiltu  46076  iccelpart  46087  isomgr  46477  isupwlk  46500  mgmpropd  46531  ismgmd  46532  ismgmhm  46539  resmgmhm  46554  iscllaw  46585  iscomlaw  46586  isasslaw  46588  isrng  46636  rngpropd  46659  c0snmgmhm  46698  zlidlring  46779  uzlidlring  46780  dmatALTval  47034  islininds  47080  lindslinindsimp2  47097  ldepsnlinc  47142  elbigo  47190  iscnrm3r  47534  isprsd  47541  lubeldm2d  47544  glbeldm2d  47545  isthincd2lem2  47609  isthincd  47610