Theorem raleqbidv 3315

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3050

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-clel 2810  df-ral 3051

This theorem is referenced by:  rspc2vd  3896  frd  5580  f12dfv  7219  f13dfv  7220  knatar  7303  ofrfvalg  7630  fmpox  8011  ovmptss  8035  frrlem4  8231  on2ind  8597  on3ind  8598  marypha1lem  9338  supeq123d  9355  oieq1  9419  acneq  9955  isfin1a  10204  fpwwe2cbv  10543  fpwwe2lem2  10545  fpwwecbv  10557  fpwwelem  10558  eltskg  10663  elgrug  10705  cau3lem  15280  rlim  15420  ello1  15440  elo1  15451  caurcvg2  15603  caucvgb  15605  fsum2dlem  15695  fsumcom2  15699  fprod2dlem  15905  fprodcom2  15909  pcfac  16829  vdwpc  16910  rami  16945  prmgaplem7  16987  prdsval  17377  ismre  17511  isacs2  17578  acsfiel  17579  iscat  17597  iscatd  17598  catidex  17599  catideu  17600  cidfval  17601  cidval  17602  catlid  17608  catrid  17609  comfeq  17631  catpropd  17634  monfval  17658  issubc  17761  fullsubc  17776  isfunc  17790  funcpropd  17828  isfull  17838  isfth  17842  fthpropd  17849  natfval  17875  initoval  17919  termoval  17920  isposd  18247  lubfval  18273  glbfval  18286  ischn  18532  chnind  18546  chnub  18547  ismgm  18568  mgmpropd  18578  ismgmd  18579  issstrmgm  18580  grpidval  18588  gsumvalx  18603  gsumpropd  18605  gsumress  18609  ismgmhm  18623  resmgmhm  18638  issgrp  18647  sgrppropd  18658  ismnddef  18663  ismndd  18683  mndpropd  18686  ismhm  18712  resmhm  18747  isgrp  18871  grppropd  18883  isgrpd2e  18887  isnsg  19086  nmznsg  19099  isghm  19146  isghmOLD  19147  isga  19222  subgga  19231  gsmsymgrfix  19359  gsmsymgreq  19363  gexval  19509  ispgp  19523  isslw  19539  sylow2blem2  19552  efgval  19648  efgi  19650  efgsdm  19661  cmnpropd  19722  iscmnd  19725  submcmn2  19770  gsumzaddlem  19852  dmdprd  19931  dprdcntz  19941  isrng  20091  rngpropd  20111  issrg  20125  isring  20174  ringpropd  20225  isirred  20357  c0snmgmhm  20400  islring  20475  rrgval  20632  isdomn  20640  sdrgacs  20736  abvfval  20745  abvpropd  20770  islmod  20817  islmodd  20819  lmodprop2d  20877  lssset  20886  islmhm  20981  reslmhm  21006  lmhmpropd  21027  islbs  21030  psgndiflemA  21558  isphl  21585  islindf  21769  islindf2  21771  lsslindf  21787  isassa  21813  isassad  21822  assapropd  21829  ltbval  22000  opsrval  22003  dmatval  22438  dmatcrng  22448  scmatcrng  22467  cpmat  22655  istopg  22841  restbas  23104  ordtrest2  23150  cnfval  23179  cnpfval  23180  ist0  23266  ist1  23267  ishaus  23268  iscnrm  23269  isnrm  23281  ist0-2  23290  ishaus2  23297  nrmsep3  23301  iscmp  23334  is1stc  23387  isptfin  23462  islocfin  23463  kgenval  23481  kgencn2  23503  txbas  23513  ptval  23516  dfac14  23564  isfil  23793  isufil  23849  isufl  23859  flfcntr  23989  ucnval  24222  iscusp  24244  prdsxmslem2  24475  tngngp3  24602  isnlm  24621  nmofval  24660  lebnumii  24923  iscau4  25237  iscmet  25242  iscmet3lem1  25249  iscmet3  25251  equivcmet  25275  ulmcaulem  26361  ulmcau  26362  fsumdvdscom  27153  dchrisumlem3  27460  pntibndlem2  27560  pntibnd  27562  pntlemp  27579  ostth2lem2  27603  madebdayim  27868  no2indslem  27934  no3inds  27938  istrkgc  28507  istrkgb  28508  istrkge  28510  trgcgrg  28568  tgcgr4  28584  isismt  28587  nbgr2vtx1edg  29404  nbuhgr2vtx1edgb  29406  uvtxval  29441  uvtxel  29442  uvtxel1  29450  uvtxusgrel  29457  cusgredg  29478  cplgr3v  29489  cplgrop  29491  usgredgsscusgredg  29514  isrgr  29614  isewlk  29657  iswlk  29665  iswwlks  29890  wlkiswwlks2  29929  isclwwlk  30040  clwlkclwwlklem1  30055  isconngr  30245  isconngr1  30246  isfrgr  30316  frgr1v  30327  nfrgr2v  30328  frgr3v  30331  1vwmgr  30332  3vfriswmgr  30334  3cyclfrgrrn1  30341  n4cyclfrgr  30347  isplig  30532  gidval  30568  vciOLD  30617  isvclem  30633  isnvlem  30666  lnoval  30808  ajfval  30865  isphg  30873  minvecolem3  30932  htth  30974  ressprs  33027  mntoval  33043  mgcoval  33047  fxpval  33226  isslmd  33263  resv1r  33399  prmidlval  33497  mxidlval  33521  rprmval  33576  isufd  33600  vieta  33715  constrconj  33881  iscref  33980  ordtrest2NEW  34059  fmcncfil  34067  issiga  34248  isrnsiga  34249  isldsys  34292  ismeas  34335  carsgval  34439  issibf  34469  sitgfval  34477  signstfvneq0  34708  istrkg2d  34802  ispconn  35396  issconn  35399  txpconn  35405  cvxpconn  35415  cvmscbv  35431  iscvm  35432  cvmsdisj  35443  cvmsss2  35447  snmlval  35504  elmrsubrn  35693  ismfs  35722  mclsval  35736  fwddifnval  36336  weiunfrlem  36637  bj-ismoore  37279  pibp19  37588  pibp21  37589  poimirlem28  37818  cover2g  37886  seqpo  37917  incsequz2  37919  caushft  37931  ismtyval  37970  isass  38016  isexid  38017  elghomlem1OLD  38055  isrngo  38067  isrngod  38068  isgrpda  38125  rngohomval  38134  iscom2  38165  idlval  38183  pridlval  38203  maxidlval  38209  elrefrels3  38769  elcnvrefrels3  38785  eleqvrels3  38847  lflset  39354  islfld  39357  isopos  39475  isoml  39533  isatl  39594  iscvlat  39618  ishlat1  39647  psubspset  40039  lautset  40377  pautsetN  40393  ldilfset  40403  ltrnfset  40412  dilfsetN  40447  trnfsetN  40450  trnsetN  40451  trlfset  40455  tendofset  41053  tendoset  41054  dihffval  41525  lpolsetN  41777  hdmapfval  42122  hgmapfval  42181  sn-isghm  42953  aomclem8  43340  islnm  43356  clsk1independent  44324  gneispace2  44410  gneispaceel2  44422  gneispacess2  44424  caucvgbf  45770  ioodvbdlimc1lem1  46212  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  issal  46595  ismea  46732  isome  46775  chnerlem1  47163  iccpartiltu  47705  iccelpart  47716  isgrim  48165  isubgrgrim  48212  isgrlim  48265  usgrexmpl2trifr  48320  gpg5nbgr3star  48364  isupwlk  48419  iscllaw  48472  iscomlaw  48473  isasslaw  48475  zlidlring  48517  uzlidlring  48518  dmatALTval  48683  islininds  48729  lindslinindsimp2  48746  ldepsnlinc  48791  elbigo  48834  iscnrm3r  49230  isprsd  49237  lubeldm2d  49240  glbeldm2d  49241  nelsubc3lem  49352  ssccatid  49354  resccatlem  49355  upciclem1  49448  upfval  49458  upfval2  49459  upfval3  49460  oppcup3lem  49488  oppcup  49489  uptr2  49503  isthincd2lem2  49717  isthincd  49718  thincpropd  49724