Theorem raleqbidv 3354

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  rspc2vd  3972  frd  5656  f12dfv  7309  f13dfv  7310  knatar  7393  ofrfvalg  7722  fmpox  8108  ovmptss  8134  frrlem4  8330  on2ind  8725  on3ind  8726  marypha1lem  9502  supeq123d  9519  oieq1  9581  acneq  10112  isfin1a  10361  fpwwe2cbv  10699  fpwwe2lem2  10701  fpwwecbv  10713  fpwwelem  10714  eltskg  10819  elgrug  10861  cau3lem  15403  rlim  15541  ello1  15561  elo1  15572  caurcvg2  15726  caucvgb  15728  fsum2dlem  15818  fsumcom2  15822  fprod2dlem  16028  fprodcom2  16032  pcfac  16946  vdwpc  17027  rami  17062  prmgaplem7  17104  prdsval  17515  ismre  17648  isacs2  17711  acsfiel  17712  iscat  17730  iscatd  17731  catidex  17732  catideu  17733  cidfval  17734  cidval  17735  catlid  17741  catrid  17742  comfeq  17764  catpropd  17767  monfval  17793  issubc  17899  fullsubc  17914  isfunc  17928  funcpropd  17967  isfull  17977  isfth  17981  fthpropd  17988  natfval  18014  initoval  18060  termoval  18061  isposd  18393  lubfval  18420  glbfval  18433  ismgm  18679  mgmpropd  18689  ismgmd  18690  issstrmgm  18691  grpidval  18699  gsumvalx  18714  gsumpropd  18716  gsumress  18720  ismgmhm  18734  resmgmhm  18749  issgrp  18758  sgrppropd  18769  ismnddef  18774  ismndd  18794  mndpropd  18797  ismhm  18820  resmhm  18855  isgrp  18979  grppropd  18991  isgrpd2e  18995  isnsg  19195  nmznsg  19208  isghm  19255  isghmOLD  19256  isga  19331  subgga  19340  gsmsymgrfix  19470  gsmsymgreq  19474  gexval  19620  ispgp  19634  isslw  19650  sylow2blem2  19663  efgval  19759  efgi  19761  efgsdm  19772  cmnpropd  19833  iscmnd  19836  submcmn2  19881  gsumzaddlem  19963  dmdprd  20042  dprdcntz  20052  isrng  20181  rngpropd  20201  issrg  20215  isring  20264  ringpropd  20311  isirred  20445  c0snmgmhm  20488  islring  20566  rrgval  20719  isdomn  20727  sdrgacs  20824  abvfval  20833  abvpropd  20858  islmod  20884  islmodd  20886  lmodprop2d  20944  lssset  20954  islmhm  21049  reslmhm  21074  lmhmpropd  21095  islbs  21098  psgndiflemA  21642  isphl  21669  islindf  21855  islindf2  21857  lsslindf  21873  isassa  21899  isassad  21908  assapropd  21915  ltbval  22084  opsrval  22087  dmatval  22519  dmatcrng  22529  scmatcrng  22548  cpmat  22736  istopg  22922  restbas  23187  ordtrest2  23233  cnfval  23262  cnpfval  23263  ist0  23349  ist1  23350  ishaus  23351  iscnrm  23352  isnrm  23364  ist0-2  23373  ishaus2  23380  nrmsep3  23384  iscmp  23417  is1stc  23470  isptfin  23545  islocfin  23546  kgenval  23564  kgencn2  23586  txbas  23596  ptval  23599  dfac14  23647  isfil  23876  isufil  23932  isufl  23942  flfcntr  24072  ucnval  24307  iscusp  24329  prdsxmslem2  24563  tngngp3  24698  isnlm  24717  nmofval  24756  lebnumii  25017  iscau4  25332  iscmet  25337  iscmet3lem1  25344  iscmet3  25346  equivcmet  25370  ulmcaulem  26455  ulmcau  26456  fsumdvdscom  27246  dchrisumlem3  27553  pntibndlem2  27653  pntibnd  27655  pntlemp  27672  ostth2lem2  27696  madebdayim  27944  no2indslem  28005  no3inds  28009  istrkgc  28480  istrkgb  28481  istrkge  28483  trgcgrg  28541  tgcgr4  28557  isismt  28560  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  uvtxval  29422  uvtxel  29423  uvtxel1  29431  uvtxusgrel  29438  cusgredg  29459  cplgr3v  29470  cplgrop  29472  usgredgsscusgredg  29495  isrgr  29595  isewlk  29638  iswlk  29646  iswwlks  29869  wlkiswwlks2  29908  isclwwlk  30016  clwlkclwwlklem1  30031  isconngr  30221  isconngr1  30222  isfrgr  30292  frgr1v  30303  nfrgr2v  30304  frgr3v  30307  1vwmgr  30308  3vfriswmgr  30310  3cyclfrgrrn1  30317  n4cyclfrgr  30323  isplig  30508  gidval  30544  vciOLD  30593  isvclem  30609  isnvlem  30642  lnoval  30784  ajfval  30841  isphg  30849  minvecolem3  30908  htth  30950  ressprs  32936  mntoval  32955  mgcoval  32959  ischn  32979  chnind  32983  chnub  32984  isslmd  33181  resv1r  33333  prmidlval  33430  mxidlval  33454  rprmval  33509  isufd  33533  constrconj  33735  iscref  33790  ordtrest2NEW  33869  fmcncfil  33877  issiga  34076  isrnsiga  34077  isldsys  34120  ismeas  34163  carsgval  34268  issibf  34298  sitgfval  34306  signstfvneq0  34549  istrkg2d  34643  ispconn  35191  issconn  35194  txpconn  35200  cvxpconn  35210  cvmscbv  35226  iscvm  35227  cvmsdisj  35238  cvmsss2  35242  snmlval  35299  elmrsubrn  35488  ismfs  35517  mclsval  35531  fwddifnval  36127  weiunfrlem  36430  bj-ismoore  37071  pibp19  37380  pibp21  37381  poimirlem28  37608  cover2g  37676  seqpo  37707  incsequz2  37709  caushft  37721  ismtyval  37760  isass  37806  isexid  37807  elghomlem1OLD  37845  isrngo  37857  isrngod  37858  isgrpda  37915  rngohomval  37924  iscom2  37955  idlval  37973  pridlval  37993  maxidlval  37999  elrefrels3  38475  elcnvrefrels3  38491  eleqvrels3  38549  lflset  39015  islfld  39018  isopos  39136  isoml  39194  isatl  39255  iscvlat  39279  ishlat1  39308  psubspset  39701  lautset  40039  pautsetN  40055  ldilfset  40065  ltrnfset  40074  dilfsetN  40109  trnfsetN  40112  trnsetN  40113  trlfset  40117  tendofset  40715  tendoset  40716  dihffval  41187  lpolsetN  41439  hdmapfval  41784  hgmapfval  41843  sn-isghm  42628  aomclem8  43018  islnm  43034  clsk1independent  44008  gneispace2  44094  gneispaceel2  44106  gneispacess2  44108  caucvgbf  45405  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  issal  46235  ismea  46372  isome  46415  iccpartiltu  47296  iccelpart  47307  isgrim  47752  isubgrgrim  47781  isgrlim  47806  usgrexmpl2trifr  47852  isupwlk  47859  iscllaw  47912  iscomlaw  47913  isasslaw  47915  zlidlring  47957  uzlidlring  47958  dmatALTval  48129  islininds  48175  lindslinindsimp2  48192  ldepsnlinc  48237  elbigo  48285  iscnrm3r  48628  isprsd  48635  lubeldm2d  48638  glbeldm2d  48639  isthincd2lem2  48703  isthincd  48704