Theorem raleqbidv 3312

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  rspc2vd  3893  frd  5571  f12dfv  7207  f13dfv  7208  knatar  7291  ofrfvalg  7618  fmpox  7999  ovmptss  8023  frrlem4  8219  on2ind  8584  on3ind  8585  marypha1lem  9317  supeq123d  9334  oieq1  9398  acneq  9934  isfin1a  10183  fpwwe2cbv  10521  fpwwe2lem2  10523  fpwwecbv  10535  fpwwelem  10536  eltskg  10641  elgrug  10683  cau3lem  15262  rlim  15402  ello1  15422  elo1  15433  caurcvg2  15585  caucvgb  15587  fsum2dlem  15677  fsumcom2  15681  fprod2dlem  15887  fprodcom2  15891  pcfac  16811  vdwpc  16892  rami  16927  prmgaplem7  16969  prdsval  17359  ismre  17492  isacs2  17559  acsfiel  17560  iscat  17578  iscatd  17579  catidex  17580  catideu  17581  cidfval  17582  cidval  17583  catlid  17589  catrid  17590  comfeq  17612  catpropd  17615  monfval  17639  issubc  17742  fullsubc  17757  isfunc  17771  funcpropd  17809  isfull  17819  isfth  17823  fthpropd  17830  natfval  17856  initoval  17900  termoval  17901  isposd  18228  lubfval  18254  glbfval  18267  ischn  18513  chnind  18527  chnub  18528  ismgm  18549  mgmpropd  18559  ismgmd  18560  issstrmgm  18561  grpidval  18569  gsumvalx  18584  gsumpropd  18586  gsumress  18590  ismgmhm  18604  resmgmhm  18619  issgrp  18628  sgrppropd  18639  ismnddef  18644  ismndd  18664  mndpropd  18667  ismhm  18693  resmhm  18728  isgrp  18852  grppropd  18864  isgrpd2e  18868  isnsg  19067  nmznsg  19080  isghm  19127  isghmOLD  19128  isga  19203  subgga  19212  gsmsymgrfix  19340  gsmsymgreq  19344  gexval  19490  ispgp  19504  isslw  19520  sylow2blem2  19533  efgval  19629  efgi  19631  efgsdm  19642  cmnpropd  19703  iscmnd  19706  submcmn2  19751  gsumzaddlem  19833  dmdprd  19912  dprdcntz  19922  isrng  20072  rngpropd  20092  issrg  20106  isring  20155  ringpropd  20206  isirred  20337  c0snmgmhm  20380  islring  20455  rrgval  20612  isdomn  20620  sdrgacs  20716  abvfval  20725  abvpropd  20750  islmod  20797  islmodd  20799  lmodprop2d  20857  lssset  20866  islmhm  20961  reslmhm  20986  lmhmpropd  21007  islbs  21010  psgndiflemA  21538  isphl  21565  islindf  21749  islindf2  21751  lsslindf  21767  isassa  21793  isassad  21802  assapropd  21809  ltbval  21978  opsrval  21981  dmatval  22407  dmatcrng  22417  scmatcrng  22436  cpmat  22624  istopg  22810  restbas  23073  ordtrest2  23119  cnfval  23148  cnpfval  23149  ist0  23235  ist1  23236  ishaus  23237  iscnrm  23238  isnrm  23250  ist0-2  23259  ishaus2  23266  nrmsep3  23270  iscmp  23303  is1stc  23356  isptfin  23431  islocfin  23432  kgenval  23450  kgencn2  23472  txbas  23482  ptval  23485  dfac14  23533  isfil  23762  isufil  23818  isufl  23828  flfcntr  23958  ucnval  24191  iscusp  24213  prdsxmslem2  24444  tngngp3  24571  isnlm  24590  nmofval  24629  lebnumii  24892  iscau4  25206  iscmet  25211  iscmet3lem1  25218  iscmet3  25220  equivcmet  25244  ulmcaulem  26330  ulmcau  26331  fsumdvdscom  27122  dchrisumlem3  27429  pntibndlem2  27529  pntibnd  27531  pntlemp  27548  ostth2lem2  27572  madebdayim  27833  no2indslem  27897  no3inds  27901  istrkgc  28432  istrkgb  28433  istrkge  28435  trgcgrg  28493  tgcgr4  28509  isismt  28512  nbgr2vtx1edg  29328  nbuhgr2vtx1edgb  29330  uvtxval  29365  uvtxel  29366  uvtxel1  29374  uvtxusgrel  29381  cusgredg  29402  cplgr3v  29413  cplgrop  29415  usgredgsscusgredg  29438  isrgr  29538  isewlk  29581  iswlk  29589  iswwlks  29814  wlkiswwlks2  29853  isclwwlk  29964  clwlkclwwlklem1  29979  isconngr  30169  isconngr1  30170  isfrgr  30240  frgr1v  30251  nfrgr2v  30252  frgr3v  30255  1vwmgr  30256  3vfriswmgr  30258  3cyclfrgrrn1  30265  n4cyclfrgr  30271  isplig  30456  gidval  30492  vciOLD  30541  isvclem  30557  isnvlem  30590  lnoval  30732  ajfval  30789  isphg  30797  minvecolem3  30856  htth  30898  ressprs  32947  mntoval  32963  mgcoval  32967  fxpval  33134  isslmd  33171  resv1r  33304  prmidlval  33402  mxidlval  33426  rprmval  33481  isufd  33505  constrconj  33758  iscref  33857  ordtrest2NEW  33936  fmcncfil  33944  issiga  34125  isrnsiga  34126  isldsys  34169  ismeas  34212  carsgval  34316  issibf  34346  sitgfval  34354  signstfvneq0  34585  istrkg2d  34679  ispconn  35267  issconn  35270  txpconn  35276  cvxpconn  35286  cvmscbv  35302  iscvm  35303  cvmsdisj  35314  cvmsss2  35318  snmlval  35375  elmrsubrn  35564  ismfs  35593  mclsval  35607  fwddifnval  36207  weiunfrlem  36508  bj-ismoore  37149  pibp19  37458  pibp21  37459  poimirlem28  37687  cover2g  37755  seqpo  37786  incsequz2  37788  caushft  37800  ismtyval  37839  isass  37885  isexid  37886  elghomlem1OLD  37924  isrngo  37936  isrngod  37937  isgrpda  37994  rngohomval  38003  iscom2  38034  idlval  38052  pridlval  38072  maxidlval  38078  elrefrels3  38610  elcnvrefrels3  38626  eleqvrels3  38688  lflset  39157  islfld  39160  isopos  39278  isoml  39336  isatl  39397  iscvlat  39421  ishlat1  39450  psubspset  39842  lautset  40180  pautsetN  40196  ldilfset  40206  ltrnfset  40215  dilfsetN  40250  trnfsetN  40253  trnsetN  40254  trlfset  40258  tendofset  40856  tendoset  40857  dihffval  41328  lpolsetN  41580  hdmapfval  41925  hgmapfval  41984  sn-isghm  42765  aomclem8  43153  islnm  43169  clsk1independent  44138  gneispace2  44224  gneispaceel2  44236  gneispacess2  44238  caucvgbf  45586  ioodvbdlimc1lem1  46028  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  issal  46411  ismea  46548  isome  46591  chnerlem1  46979  iccpartiltu  47521  iccelpart  47532  isgrim  47981  isubgrgrim  48028  isgrlim  48081  usgrexmpl2trifr  48136  gpg5nbgr3star  48180  isupwlk  48235  iscllaw  48288  iscomlaw  48289  isasslaw  48291  zlidlring  48333  uzlidlring  48334  dmatALTval  48500  islininds  48546  lindslinindsimp2  48563  ldepsnlinc  48608  elbigo  48651  iscnrm3r  49047  isprsd  49054  lubeldm2d  49057  glbeldm2d  49058  nelsubc3lem  49170  ssccatid  49172  resccatlem  49173  upciclem1  49266  upfval  49276  upfval2  49277  upfval3  49278  oppcup3lem  49306  oppcup  49307  uptr2  49321  isthincd2lem2  49535  isthincd  49536  thincpropd  49542