Theorem raleqbidv 3343

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-ral 3059

This theorem is referenced by:  rspc2vd  3958  frd  5644  f12dfv  7292  f13dfv  7293  knatar  7376  ofrfvalg  7704  fmpox  8090  ovmptss  8116  frrlem4  8312  on2ind  8705  on3ind  8706  marypha1lem  9470  supeq123d  9487  oieq1  9549  acneq  10080  isfin1a  10329  fpwwe2cbv  10667  fpwwe2lem2  10669  fpwwecbv  10681  fpwwelem  10682  eltskg  10787  elgrug  10829  cau3lem  15389  rlim  15527  ello1  15547  elo1  15558  caurcvg2  15710  caucvgb  15712  fsum2dlem  15802  fsumcom2  15806  fprod2dlem  16012  fprodcom2  16016  pcfac  16932  vdwpc  17013  rami  17048  prmgaplem7  17090  prdsval  17501  ismre  17634  isacs2  17697  acsfiel  17698  iscat  17716  iscatd  17717  catidex  17718  catideu  17719  cidfval  17720  cidval  17721  catlid  17727  catrid  17728  comfeq  17750  catpropd  17753  monfval  17779  issubc  17885  fullsubc  17900  isfunc  17914  funcpropd  17953  isfull  17963  isfth  17967  fthpropd  17974  natfval  18000  initoval  18046  termoval  18047  isposd  18380  lubfval  18407  glbfval  18420  ismgm  18666  mgmpropd  18676  ismgmd  18677  issstrmgm  18678  grpidval  18686  gsumvalx  18701  gsumpropd  18703  gsumress  18707  ismgmhm  18721  resmgmhm  18736  issgrp  18745  sgrppropd  18756  ismnddef  18761  ismndd  18781  mndpropd  18784  ismhm  18810  resmhm  18845  isgrp  18969  grppropd  18981  isgrpd2e  18985  isnsg  19185  nmznsg  19198  isghm  19245  isghmOLD  19246  isga  19321  subgga  19330  gsmsymgrfix  19460  gsmsymgreq  19464  gexval  19610  ispgp  19624  isslw  19640  sylow2blem2  19653  efgval  19749  efgi  19751  efgsdm  19762  cmnpropd  19823  iscmnd  19826  submcmn2  19871  gsumzaddlem  19953  dmdprd  20032  dprdcntz  20042  isrng  20171  rngpropd  20191  issrg  20205  isring  20254  ringpropd  20301  isirred  20435  c0snmgmhm  20478  islring  20556  rrgval  20713  isdomn  20721  sdrgacs  20818  abvfval  20827  abvpropd  20852  islmod  20878  islmodd  20880  lmodprop2d  20938  lssset  20948  islmhm  21043  reslmhm  21068  lmhmpropd  21089  islbs  21092  psgndiflemA  21636  isphl  21663  islindf  21849  islindf2  21851  lsslindf  21867  isassa  21893  isassad  21902  assapropd  21909  ltbval  22078  opsrval  22081  dmatval  22513  dmatcrng  22523  scmatcrng  22542  cpmat  22730  istopg  22916  restbas  23181  ordtrest2  23227  cnfval  23256  cnpfval  23257  ist0  23343  ist1  23344  ishaus  23345  iscnrm  23346  isnrm  23358  ist0-2  23367  ishaus2  23374  nrmsep3  23378  iscmp  23411  is1stc  23464  isptfin  23539  islocfin  23540  kgenval  23558  kgencn2  23580  txbas  23590  ptval  23593  dfac14  23641  isfil  23870  isufil  23926  isufl  23936  flfcntr  24066  ucnval  24301  iscusp  24323  prdsxmslem2  24557  tngngp3  24692  isnlm  24711  nmofval  24750  lebnumii  25011  iscau4  25326  iscmet  25331  iscmet3lem1  25338  iscmet3  25340  equivcmet  25364  ulmcaulem  26451  ulmcau  26452  fsumdvdscom  27242  dchrisumlem3  27549  pntibndlem2  27649  pntibnd  27651  pntlemp  27668  ostth2lem2  27692  madebdayim  27940  no2indslem  28001  no3inds  28005  istrkgc  28476  istrkgb  28477  istrkge  28479  trgcgrg  28537  tgcgr4  28553  isismt  28556  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  uvtxval  29418  uvtxel  29419  uvtxel1  29427  uvtxusgrel  29434  cusgredg  29455  cplgr3v  29466  cplgrop  29468  usgredgsscusgredg  29491  isrgr  29591  isewlk  29634  iswlk  29642  iswwlks  29865  wlkiswwlks2  29904  isclwwlk  30012  clwlkclwwlklem1  30027  isconngr  30217  isconngr1  30218  isfrgr  30288  frgr1v  30299  nfrgr2v  30300  frgr3v  30303  1vwmgr  30304  3vfriswmgr  30306  3cyclfrgrrn1  30313  n4cyclfrgr  30319  isplig  30504  gidval  30540  vciOLD  30589  isvclem  30605  isnvlem  30638  lnoval  30780  ajfval  30837  isphg  30845  minvecolem3  30904  htth  30946  ressprs  32938  mntoval  32956  mgcoval  32960  ischn  32980  chnind  32984  chnub  32985  isslmd  33190  resv1r  33347  prmidlval  33444  mxidlval  33468  rprmval  33523  isufd  33547  constrconj  33749  iscref  33804  ordtrest2NEW  33883  fmcncfil  33891  issiga  34092  isrnsiga  34093  isldsys  34136  ismeas  34179  carsgval  34284  issibf  34314  sitgfval  34322  signstfvneq0  34565  istrkg2d  34659  ispconn  35207  issconn  35210  txpconn  35216  cvxpconn  35226  cvmscbv  35242  iscvm  35243  cvmsdisj  35254  cvmsss2  35258  snmlval  35315  elmrsubrn  35504  ismfs  35533  mclsval  35547  fwddifnval  36144  weiunfrlem  36446  bj-ismoore  37087  pibp19  37396  pibp21  37397  poimirlem28  37634  cover2g  37702  seqpo  37733  incsequz2  37735  caushft  37747  ismtyval  37786  isass  37832  isexid  37833  elghomlem1OLD  37871  isrngo  37883  isrngod  37884  isgrpda  37941  rngohomval  37950  iscom2  37981  idlval  37999  pridlval  38019  maxidlval  38025  elrefrels3  38500  elcnvrefrels3  38516  eleqvrels3  38574  lflset  39040  islfld  39043  isopos  39161  isoml  39219  isatl  39280  iscvlat  39304  ishlat1  39333  psubspset  39726  lautset  40064  pautsetN  40080  ldilfset  40090  ltrnfset  40099  dilfsetN  40134  trnfsetN  40137  trnsetN  40138  trlfset  40142  tendofset  40740  tendoset  40741  dihffval  41212  lpolsetN  41464  hdmapfval  41809  hgmapfval  41868  sn-isghm  42659  aomclem8  43049  islnm  43065  clsk1independent  44035  gneispace2  44121  gneispaceel2  44133  gneispacess2  44135  caucvgbf  45439  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  issal  46269  ismea  46406  isome  46449  iccpartiltu  47346  iccelpart  47357  isgrim  47805  isubgrgrim  47834  isgrlim  47884  usgrexmpl2trifr  47931  gpg5nbgr3star  47971  isupwlk  47979  iscllaw  48032  iscomlaw  48033  isasslaw  48035  zlidlring  48077  uzlidlring  48078  dmatALTval  48245  islininds  48291  lindslinindsimp2  48308  ldepsnlinc  48353  elbigo  48400  iscnrm3r  48744  isprsd  48751  lubeldm2d  48754  glbeldm2d  48755  upciclem1  48811  isthincd2lem2  48835  isthincd  48836