Theorem raleqbidv 3342

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  rspc2vd  3944  frd  5635  f12dfv  7273  f13dfv  7274  knatar  7356  ofrfvalg  7680  fmpox  8055  ovmptss  8081  frrlem4  8276  on2ind  8670  on3ind  8671  marypha1lem  9430  supeq123d  9447  oieq1  9509  acneq  10040  isfin1a  10289  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwecbv  10641  fpwwelem  10642  eltskg  10747  elgrug  10789  cau3lem  15303  rlim  15441  ello1  15461  elo1  15472  caurcvg2  15626  caucvgb  15628  fsum2dlem  15718  fsumcom2  15722  fprod2dlem  15926  fprodcom2  15930  pcfac  16834  vdwpc  16915  rami  16950  prmgaplem7  16992  prdsval  17403  ismre  17536  isacs2  17599  acsfiel  17600  iscat  17618  iscatd  17619  catidex  17620  catideu  17621  cidfval  17622  cidval  17623  catlid  17629  catrid  17630  comfeq  17652  catpropd  17655  monfval  17681  issubc  17787  fullsubc  17802  isfunc  17816  funcpropd  17853  isfull  17863  isfth  17867  fthpropd  17874  natfval  17899  initoval  17945  termoval  17946  isposd  18278  lubfval  18305  glbfval  18318  ismgm  18564  issstrmgm  18574  grpidval  18582  gsumvalx  18597  gsumpropd  18599  gsumress  18603  issgrp  18613  sgrppropd  18624  ismnddef  18629  ismndd  18649  mndpropd  18652  ismhm  18675  resmhm  18703  isgrp  18827  grppropd  18839  isgrpd2e  18843  isnsg  19037  nmznsg  19050  isghm  19094  isga  19157  subgga  19166  gsmsymgrfix  19298  gsmsymgreq  19302  gexval  19448  ispgp  19462  isslw  19478  sylow2blem2  19491  efgval  19587  efgi  19589  efgsdm  19600  cmnpropd  19661  iscmnd  19664  submcmn2  19709  gsumzaddlem  19791  dmdprd  19870  dprdcntz  19880  issrg  20013  isring  20062  ringpropd  20104  isirred  20237  islring  20314  sdrgacs  20421  abvfval  20430  abvpropd  20454  islmod  20479  islmodd  20481  lmodprop2d  20539  lssset  20549  islmhm  20643  reslmhm  20668  lmhmpropd  20689  islbs  20692  rrgval  20909  isdomn  20916  psgndiflemA  21160  isphl  21187  islindf  21373  islindf2  21375  lsslindf  21391  isassa  21417  isassad  21425  assapropd  21432  ltbval  21604  opsrval  21607  dmatval  22001  dmatcrng  22011  scmatcrng  22030  cpmat  22218  istopg  22404  restbas  22669  ordtrest2  22715  cnfval  22744  cnpfval  22745  ist0  22831  ist1  22832  ishaus  22833  iscnrm  22834  isnrm  22846  ist0-2  22855  ishaus2  22862  nrmsep3  22866  iscmp  22899  is1stc  22952  isptfin  23027  islocfin  23028  kgenval  23046  kgencn2  23068  txbas  23078  ptval  23081  dfac14  23129  isfil  23358  isufil  23414  isufl  23424  flfcntr  23554  ucnval  23789  iscusp  23811  prdsxmslem2  24045  tngngp3  24180  isnlm  24199  nmofval  24238  lebnumii  24489  iscau4  24803  iscmet  24808  iscmet3lem1  24815  iscmet3  24817  equivcmet  24841  ulmcaulem  25913  ulmcau  25914  fsumdvdscom  26696  dchrisumlem3  27001  pntibndlem2  27101  pntibnd  27103  pntlemp  27120  ostth2lem2  27144  madebdayim  27390  no2indslem  27447  no3inds  27451  istrkgc  27743  istrkgb  27744  istrkge  27746  trgcgrg  27804  tgcgr4  27820  isismt  27823  nbgr2vtx1edg  28645  nbuhgr2vtx1edgb  28647  uvtxval  28682  uvtxel  28683  uvtxel1  28691  uvtxusgrel  28698  cusgredg  28719  cplgr3v  28730  cplgrop  28732  usgredgsscusgredg  28754  isrgr  28854  isewlk  28897  iswlk  28905  iswwlks  29128  wlkiswwlks2  29167  isclwwlk  29275  clwlkclwwlklem1  29290  isconngr  29480  isconngr1  29481  isfrgr  29551  frgr1v  29562  nfrgr2v  29563  frgr3v  29566  1vwmgr  29567  3vfriswmgr  29569  3cyclfrgrrn1  29576  n4cyclfrgr  29582  isplig  29767  gidval  29803  vciOLD  29852  isvclem  29868  isnvlem  29901  lnoval  30043  ajfval  30100  isphg  30108  minvecolem3  30167  htth  30209  ressprs  32171  mntoval  32190  mgcoval  32194  isslmd  32388  resv1r  32497  prmidlval  32600  mxidlval  32622  isufd  32677  rprmval  32678  iscref  32893  ordtrest2NEW  32972  fmcncfil  32980  issiga  33179  isrnsiga  33180  isldsys  33223  ismeas  33266  carsgval  33371  issibf  33401  sitgfval  33409  signstfvneq0  33652  istrkg2d  33747  ispconn  34283  issconn  34286  txpconn  34292  cvxpconn  34302  cvmscbv  34318  iscvm  34319  cvmsdisj  34330  cvmsss2  34334  snmlval  34391  elmrsubrn  34580  ismfs  34609  mclsval  34623  fwddifnval  35204  bj-ismoore  36072  pibp19  36381  pibp21  36382  poimirlem28  36602  cover2g  36670  seqpo  36701  incsequz2  36703  caushft  36715  ismtyval  36754  isass  36800  isexid  36801  elghomlem1OLD  36839  isrngo  36851  isrngod  36852  isgrpda  36909  rngohomval  36918  iscom2  36949  idlval  36967  pridlval  36987  maxidlval  36993  elrefrels3  37475  elcnvrefrels3  37491  eleqvrels3  37549  lflset  38015  islfld  38018  isopos  38136  isoml  38194  isatl  38255  iscvlat  38279  ishlat1  38308  psubspset  38701  lautset  39039  pautsetN  39055  ldilfset  39065  ltrnfset  39074  dilfsetN  39109  trnfsetN  39112  trnsetN  39113  trlfset  39117  tendofset  39715  tendoset  39716  dihffval  40187  lpolsetN  40439  hdmapfval  40784  hgmapfval  40843  aomclem8  41885  islnm  41901  clsk1independent  42879  gneispace2  42965  gneispaceel2  42977  gneispacess2  42979  caucvgbf  44279  ioodvbdlimc1lem1  44726  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  issal  45109  ismea  45246  isome  45289  iccpartiltu  46169  iccelpart  46180  isomgr  46570  isupwlk  46593  mgmpropd  46624  ismgmd  46625  ismgmhm  46632  resmgmhm  46647  iscllaw  46678  iscomlaw  46679  isasslaw  46681  isrng  46729  rngpropd  46752  c0snmgmhm  46792  zlidlring  46905  uzlidlring  46906  dmatALTval  47159  islininds  47205  lindslinindsimp2  47222  ldepsnlinc  47267  elbigo  47315  iscnrm3r  47659  isprsd  47666  lubeldm2d  47669  glbeldm2d  47670  isthincd2lem2  47734  isthincd  47735