Theorem raleqbidv 3334

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rspc2vd  3894  frd  5607  f12dfv  7281  f13dfv  7282  knatar  7367  ofrfvalg  7701  fmpox  8078  ovmptss  8104  frrlem4  8307  on2ind  8678  on3ind  8679  marypha1lem  9425  supeq123d  9442  oieq1  9506  acneq  10122  isfin1a  10370  fpwwe2cbv  10715  fpwwe2lem2  10717  fpwwecbv  10729  fpwwelem  10730  eltskg  10835  elgrug  10877  cau3lem  15522  rlim  15662  ello1  15682  elo1  15693  caurcvg2  15845  caucvgb  15847  fsum2dlem  15936  fsumcom2  15940  fprod2dlem  16147  fprodcom2  16151  pcfac  17077  vdwpc  17158  rami  17193  prmgaplem7  17235  prdsval  17626  ismre  17760  isacs2  17827  acsfiel  17828  iscat  17846  iscatd  17847  catidex  17848  catideu  17849  cidfval  17850  cidval  17851  catlid  17857  catrid  17858  comfeq  17880  catpropd  17883  monfval  17907  issubc  18010  fullsubc  18025  isfunc  18039  funcpropd  18077  isfull  18087  isfth  18091  fthpropd  18098  natfval  18124  initoval  18168  termoval  18169  isposd  18496  lubfval  18522  glbfval  18535  ischn  18781  chnind  18795  chnub  18796  ismgm  18817  mgmpropd  18829  ismgmd  18830  issstrmgm  18831  grpidval  18840  idressid  18862  gsumvalx  18865  gsumpropd  18867  gsumress  18871  ismgmhm  18885  resmgmhm  18900  issgrp  18909  sgrppropd  18920  ismnddef  18925  ismndd  18946  mndpropd  18951  ismhm  18980  resmhm  19016  isgrp  19150  grppropd  19162  isgrpd2e  19166  isnsg  19365  nmznsg  19378  isghm  19430  isga  19505  subgga  19514  gsmsymgrfix  19642  gsmsymgreq  19646  gexval  19792  ispgp  19806  isslw  19822  sylow2blem2  19835  efgval  19931  efgi  19933  efgsdm  19944  cmnpropd  20005  iscmnd  20008  submcmn2  20053  gsumzaddlem  20135  dmdprd  20214  dprdcntz  20224  isrng  20376  rngpropd  20396  issrg  20414  isring  20463  ringpropd  20519  isirred  20649  c0snmgmhm  20692  islring  20792  rrgval  20949  isdomn  20957  sdrgacs  21058  abvfval  21067  abvpropd  21092  islmod  21139  islmodd  21141  lmodprop2d  21199  lssset  21208  islmhm  21302  reslmhm  21327  lmhmpropd  21348  islbs  21351  prmidlval  21618  psgndiflemA  21907  isphl  21934  islindf  22118  islindf2  22120  lsslindf  22136  isassa  22164  isassad  22173  assapropd  22179  ltbval  22352  opsrval  22355  dmatval  22807  dmatcrng  22817  scmatcrng  22836  cpmat  23027  istopg  23213  restbas  23476  ordtrest2  23522  cnfval  23551  cnpfval  23552  ist0  23638  ist1  23639  ishaus  23640  iscnrm  23641  isnrm  23653  ist0-2  23662  ishaus2  23669  nrmsep3  23673  iscmp  23706  is1stc  23759  isptfin  23835  islocfin  23836  kgenval  23854  kgencn2  23876  txbas  23886  ptval  23889  dfac14  23937  isfil  24166  isufil  24222  isufl  24232  flfcntr  24362  ucnval  24595  iscusp  24617  prdsxmslem2  24848  tngngp3  24975  isnlm  24994  nmofval  25033  lebnumii  25287  iscau4  25600  iscmet  25605  iscmet3lem1  25612  iscmet3  25614  equivcmet  25638  ulmcaulem  26721  ulmcau  26722  fsumdvdscom  27512  dchrisumlem3  27818  pntibndlem2  27918  pntibnd  27920  pntlemp  27937  ostth2lem2  27961  madebdayim  28274  no2indlesm  28340  no3inds  28344  istrkgc  28916  istrkgb  28917  istrkge  28919  trgcgrg  28978  tgcgr4  28994  isismt  28997  nbgr2vtx1edg  29931  nbuhgr2vtx1edgb  29933  uvtxval  29968  uvtxel  29969  uvtxel1  29977  uvtxusgrel  29984  cusgredg  30005  cplgr3v  30016  cplgrop  30018  usgredgsscusgredg  30040  isrgr  30140  isewlk  30183  iswlk  30191  iswwlks  30425  wlkiswwlks2  30464  isclwwlk  30575  clwlkclwwlklem1  30590  isconngr  30790  isconngr1  30791  isfrgr  30861  frgr1v  30872  nfrgr2v  30873  frgr3v  30876  1vwmgr  30877  3vfriswmgr  30879  3cyclfrgrrn1  30886  n4cyclfrgr  30892  isplig  31078  gidval  31114  vciOLD  31163  isvclem  31179  isnvlem  31212  lnoval  31354  ajfval  31411  isphg  31419  minvecolem3  31478  htth  31520  ressprs  33527  mntoval  33543  mgcoval  33547  fxpval  33726  isslmd  33763  resv1r  33900  mxidlval  33986  rprmval  34048  isufd  34072  vieta  34212  constrconj  34377  iscref  34476  ordtrest2NEW  34555  fmcncfil  34563  issiga  34744  isrnsiga  34745  isldsys  34789  ismeas  34832  carsgval  34935  issibf  34965  sitgfval  34973  signstfvneq0  35201  istrkg2d  35295  ispconn  35988  issconn  35991  txpconn  35997  cvxpconn  36007  cvmscbv  36023  iscvm  36024  cvmsdisj  36035  cvmsss2  36039  snmlval  36096  elmrsubrn  36285  ismfs  36314  mclsval  36328  fwddifnval  36928  weiunfrlem  37252  bj-ismoore  38026  pibp19  38338  pibp21  38339  poimirlem28  38567  cover2g  38651  seqpo  38682  incsequz2  38684  caushft  38696  ismtyval  38735  isass  38781  isexid  38782  elghomlem1OLD  38820  isrngo  38832  isrngod  38833  isgrpda  38890  rngohomval  38899  iscom2  38930  idlval  38948  pridlval  38968  maxidlval  38974  elrefrels3  39532  elcnvrefrels3  39548  eleqvrels3  39610  lflset  40117  islfld  40120  isopos  40238  isoml  40296  isatl  40357  iscvlat  40381  ishlat1  40410  psubspset  40802  lautset  41140  pautsetN  41156  ldilfset  41166  ltrnfset  41175  dilfsetN  41210  trnfsetN  41213  trnsetN  41214  trlfset  41218  tendofset  41816  tendoset  41817  dihffval  42288  lpolsetN  42540  hdmapfval  42885  hgmapfval  42944  sn-isghm  43685  aomclem8  44063  islnm  44079  clsk1independent  45046  gneispace2  45132  gneispaceel2  45144  gneispacess2  45146  caucvgbf  46499  ioodvbdlimc1lem1  46941  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  issal  47324  ismea  47461  isome  47504  chnerlem1  47892  tmachlem-agreesn  47957  iccpartiltu  48504  iccelpart  48515  isgrim  48980  isubgrgrim  49027  isgrlim  49080  usgrexmpl2trifr  49135  gpg5nbgr3star  49179  isupwlk  49234  iscllaw  49286  iscomlaw  49287  isasslaw  49289  zlidlring  49331  uzlidlring  49332  dmatALTval  49512  islininds  49558  lindslinindsimp2  49575  ldepsnlinc  49620  elbigo  49663  iscnrm3r  50056  isprsd  50063  lubeldm2d  50066  glbeldm2d  50067  nelsubc3lem  50178  ssccatid  50180  resccatlem  50181  upciclem1  50274  upfval  50284  upfval2  50285  upfval3  50286  oppcup3lem  50314  oppcup  50315  uptr2  50329  isthincd2lem2  50543  isthincd  50544  thincpropd  50550