Theorem raleqbidv 3335

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 2824	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	imbi12d 345	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))
5	4	ralbidv2 3116	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-ral 3069

This theorem is referenced by:  rspc2vd  3884  frd  5545  f12dfv  7139  f13dfv  7140  knatar  7222  ofrfvalg  7533  fmpox  7898  ovmptss  7922  frrlem4  8094  marypha1lem  9181  supeq123d  9198  oieq1  9260  acneq  9788  isfin1a  10037  fpwwe2cbv  10375  fpwwe2lem2  10377  fpwwecbv  10389  fpwwelem  10390  eltskg  10495  elgrug  10537  cau3lem  15055  rlim  15193  ello1  15213  elo1  15224  caurcvg2  15378  caucvgb  15380  fsum2dlem  15471  fsumcom2  15475  fprod2dlem  15679  fprodcom2  15683  pcfac  16589  vdwpc  16670  rami  16705  prmgaplem7  16747  prdsval  17155  ismre  17288  isacs2  17351  acsfiel  17352  iscat  17370  iscatd  17371  catidex  17372  catideu  17373  cidfval  17374  cidval  17375  catlid  17381  catrid  17382  comfeq  17404  catpropd  17407  monfval  17433  issubc  17539  fullsubc  17554  isfunc  17568  funcpropd  17605  isfull  17615  isfth  17619  fthpropd  17626  natfval  17651  initoval  17697  termoval  17698  isposd  18030  lubfval  18057  glbfval  18070  ismgm  18316  issstrmgm  18326  grpidval  18334  gsumvalx  18349  gsumpropd  18351  gsumress  18355  issgrp  18365  ismnddef  18376  ismndd  18396  mndpropd  18399  ismhm  18421  resmhm  18448  isgrp  18572  grppropd  18583  isgrpd2e  18587  isnsg  18772  nmznsg  18785  isghm  18823  isga  18886  subgga  18895  gsmsymgrfix  19025  gsmsymgreq  19029  gexval  19172  ispgp  19186  isslw  19202  sylow2blem2  19215  efgval  19312  efgi  19314  efgsdm  19325  cmnpropd  19385  iscmnd  19388  submcmn2  19429  gsumzaddlem  19511  dmdprd  19590  dprdcntz  19600  issrg  19732  isring  19776  ringpropd  19810  isirred  19930  sdrgacs  20058  abvfval  20067  abvpropd  20091  islmod  20116  islmodd  20118  lmodprop2d  20174  lssset  20184  islmhm  20278  reslmhm  20303  lmhmpropd  20324  islbs  20327  rrgval  20547  isdomn  20554  psgndiflemA  20795  isphl  20822  islindf  21008  islindf2  21010  lsslindf  21026  isassa  21052  isassad  21060  assapropd  21065  ltbval  21233  opsrval  21236  dmatval  21630  dmatcrng  21640  scmatcrng  21659  cpmat  21847  istopg  22033  restbas  22298  ordtrest2  22344  cnfval  22373  cnpfval  22374  ist0  22460  ist1  22461  ishaus  22462  iscnrm  22463  isnrm  22475  ist0-2  22484  ishaus2  22491  nrmsep3  22495  iscmp  22528  is1stc  22581  isptfin  22656  islocfin  22657  kgenval  22675  kgencn2  22697  txbas  22707  ptval  22710  dfac14  22758  isfil  22987  isufil  23043  isufl  23053  flfcntr  23183  ucnval  23418  iscusp  23440  prdsxmslem2  23674  tngngp3  23809  isnlm  23828  nmofval  23867  lebnumii  24118  iscau4  24432  iscmet  24437  iscmet3lem1  24444  iscmet3  24446  equivcmet  24470  ulmcaulem  25542  ulmcau  25543  fsumdvdscom  26323  dchrisumlem3  26628  pntibndlem2  26728  pntibnd  26730  pntlemp  26747  ostth2lem2  26771  trgcgrg  26865  tgcgr4  26881  isismt  26884  nbgr2vtx1edg  27706  nbuhgr2vtx1edgb  27708  uvtxval  27743  uvtxel  27744  uvtxel1  27752  uvtxusgrel  27759  cusgredg  27780  cplgr3v  27791  cplgrop  27793  usgredgsscusgredg  27815  isrgr  27915  isewlk  27958  iswlk  27966  iswwlks  28188  wlkiswwlks2  28227  isclwwlk  28335  clwlkclwwlklem1  28350  isconngr  28540  isconngr1  28541  isfrgr  28611  frgr1v  28622  nfrgr2v  28623  frgr3v  28626  1vwmgr  28627  3vfriswmgr  28629  3cyclfrgrrn1  28636  n4cyclfrgr  28642  isplig  28825  gidval  28861  vciOLD  28910  isvclem  28926  isnvlem  28959  lnoval  29101  ajfval  29158  isphg  29166  minvecolem3  29225  htth  29267  ressprs  31228  mntoval  31247  mgcoval  31251  isslmd  31442  resv1r  31528  prmidlval  31599  mxidlval  31620  isufd  31650  rprmval  31651  iscref  31781  ordtrest2NEW  31860  fmcncfil  31868  issiga  32067  isrnsiga  32068  isldsys  32111  ismeas  32154  carsgval  32257  issibf  32287  sitgfval  32295  signstfvneq0  32538  istrkg2d  32633  ispconn  33172  issconn  33175  txpconn  33181  cvxpconn  33191  cvmscbv  33207  iscvm  33208  cvmsdisj  33219  cvmsss2  33223  snmlval  33280  elmrsubrn  33469  ismfs  33498  mclsval  33512  on2ind  33815  on3ind  33816  madebdayim  34057  no2indslem  34098  no3inds  34102  fwddifnval  34452  bj-ismoore  35263  pibp19  35572  pibp21  35573  poimirlem28  35792  cover2g  35860  seqpo  35892  incsequz2  35894  caushft  35906  ismtyval  35945  isass  35991  isexid  35992  elghomlem1OLD  36030  isrngo  36042  isrngod  36043  isgrpda  36100  rngohomval  36109  iscom2  36140  idlval  36158  pridlval  36178  maxidlval  36184  elrefrels3  36623  elcnvrefrels3  36636  eleqvrels3  36693  lflset  37060  islfld  37063  isopos  37181  isoml  37239  isatl  37300  iscvlat  37324  ishlat1  37353  psubspset  37745  lautset  38083  pautsetN  38099  ldilfset  38109  ltrnfset  38118  dilfsetN  38153  trnfsetN  38156  trnsetN  38157  trlfset  38161  tendofset  38759  tendoset  38760  dihffval  39231  lpolsetN  39483  hdmapfval  39828  hgmapfval  39887  aomclem8  40873  islnm  40889  clsk1independent  41616  gneispace2  41702  gneispaceel2  41714  gneispacess2  41716  ioodvbdlimc1lem1  43432  ioodvbdlimc1lem2  43433  ioodvbdlimc2lem  43435  issal  43815  ismea  43949  isome  43992  iccpartiltu  44831  iccelpart  44842  isomgr  45232  isupwlk  45255  mgmpropd  45286  ismgmd  45287  ismgmhm  45294  resmgmhm  45309  iscllaw  45340  iscomlaw  45341  isasslaw  45343  isrng  45391  c0snmgmhm  45429  zlidlring  45443  uzlidlring  45444  dmatALTval  45698  islininds  45744  lindslinindsimp2  45761  ldepsnlinc  45806  elbigo  45854  iscnrm3r  46199  isprsd  46206  lubeldm2d  46209  glbeldm2d  46210  isthincd2lem2  46274  isthincd  46275