Theorem raleqbidv 3312

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rspc2vd  3886  frd  5583  f12dfv  7223  f13dfv  7224  knatar  7307  ofrfvalg  7634  fmpox  8015  ovmptss  8038  frrlem4  8234  on2ind  8600  on3ind  8601  marypha1lem  9341  supeq123d  9358  oieq1  9422  acneq  9960  isfin1a  10209  fpwwe2cbv  10548  fpwwe2lem2  10550  fpwwecbv  10562  fpwwelem  10563  eltskg  10668  elgrug  10710  cau3lem  15312  rlim  15452  ello1  15472  elo1  15483  caurcvg2  15635  caucvgb  15637  fsum2dlem  15727  fsumcom2  15731  fprod2dlem  15940  fprodcom2  15944  pcfac  16865  vdwpc  16946  rami  16981  prmgaplem7  17023  prdsval  17413  ismre  17547  isacs2  17614  acsfiel  17615  iscat  17633  iscatd  17634  catidex  17635  catideu  17636  cidfval  17637  cidval  17638  catlid  17644  catrid  17645  comfeq  17667  catpropd  17670  monfval  17694  issubc  17797  fullsubc  17812  isfunc  17826  funcpropd  17864  isfull  17874  isfth  17878  fthpropd  17885  natfval  17911  initoval  17955  termoval  17956  isposd  18283  lubfval  18309  glbfval  18322  ischn  18568  chnind  18582  chnub  18583  ismgm  18604  mgmpropd  18614  ismgmd  18615  issstrmgm  18616  grpidval  18624  gsumvalx  18639  gsumpropd  18641  gsumress  18645  ismgmhm  18659  resmgmhm  18674  issgrp  18683  sgrppropd  18694  ismnddef  18699  ismndd  18719  mndpropd  18722  ismhm  18748  resmhm  18783  isgrp  18910  grppropd  18922  isgrpd2e  18926  isnsg  19125  nmznsg  19138  isghm  19185  isghmOLD  19186  isga  19261  subgga  19270  gsmsymgrfix  19398  gsmsymgreq  19402  gexval  19548  ispgp  19562  isslw  19578  sylow2blem2  19591  efgval  19687  efgi  19689  efgsdm  19700  cmnpropd  19761  iscmnd  19764  submcmn2  19809  gsumzaddlem  19891  dmdprd  19970  dprdcntz  19980  isrng  20130  rngpropd  20150  issrg  20164  isring  20213  ringpropd  20264  isirred  20394  c0snmgmhm  20437  islring  20512  rrgval  20669  isdomn  20677  sdrgacs  20773  abvfval  20782  abvpropd  20807  islmod  20854  islmodd  20856  lmodprop2d  20914  lssset  20923  islmhm  21018  reslmhm  21043  lmhmpropd  21064  islbs  21067  psgndiflemA  21595  isphl  21622  islindf  21806  islindf2  21808  lsslindf  21824  isassa  21850  isassad  21859  assapropd  21865  ltbval  22035  opsrval  22038  dmatval  22471  dmatcrng  22481  scmatcrng  22500  cpmat  22688  istopg  22874  restbas  23137  ordtrest2  23183  cnfval  23212  cnpfval  23213  ist0  23299  ist1  23300  ishaus  23301  iscnrm  23302  isnrm  23314  ist0-2  23323  ishaus2  23330  nrmsep3  23334  iscmp  23367  is1stc  23420  isptfin  23495  islocfin  23496  kgenval  23514  kgencn2  23536  txbas  23546  ptval  23549  dfac14  23597  isfil  23826  isufil  23882  isufl  23892  flfcntr  24022  ucnval  24255  iscusp  24277  prdsxmslem2  24508  tngngp3  24635  isnlm  24654  nmofval  24693  lebnumii  24947  iscau4  25260  iscmet  25265  iscmet3lem1  25272  iscmet3  25274  equivcmet  25298  ulmcaulem  26376  ulmcau  26377  fsumdvdscom  27166  dchrisumlem3  27472  pntibndlem2  27572  pntibnd  27574  pntlemp  27591  ostth2lem2  27615  madebdayim  27898  no2indlesm  27964  no3inds  27968  istrkgc  28540  istrkgb  28541  istrkge  28543  trgcgrg  28601  tgcgr4  28617  isismt  28620  nbgr2vtx1edg  29437  nbuhgr2vtx1edgb  29439  uvtxval  29474  uvtxel  29475  uvtxel1  29483  uvtxusgrel  29490  cusgredg  29511  cplgr3v  29522  cplgrop  29524  usgredgsscusgredg  29547  isrgr  29647  isewlk  29690  iswlk  29698  iswwlks  29923  wlkiswwlks2  29962  isclwwlk  30073  clwlkclwwlklem1  30088  isconngr  30278  isconngr1  30279  isfrgr  30349  frgr1v  30360  nfrgr2v  30361  frgr3v  30364  1vwmgr  30365  3vfriswmgr  30367  3cyclfrgrrn1  30374  n4cyclfrgr  30380  isplig  30566  gidval  30602  vciOLD  30651  isvclem  30667  isnvlem  30700  lnoval  30842  ajfval  30899  isphg  30907  minvecolem3  30966  htth  31008  ressprs  33045  mntoval  33061  mgcoval  33065  fxpval  33245  isslmd  33282  resv1r  33418  prmidlval  33516  mxidlval  33540  rprmval  33595  isufd  33619  vieta  33743  constrconj  33909  iscref  34008  ordtrest2NEW  34087  fmcncfil  34095  issiga  34276  isrnsiga  34277  isldsys  34320  ismeas  34363  carsgval  34467  issibf  34497  sitgfval  34505  signstfvneq0  34736  istrkg2d  34830  ispconn  35425  issconn  35428  txpconn  35434  cvxpconn  35444  cvmscbv  35460  iscvm  35461  cvmsdisj  35472  cvmsss2  35476  snmlval  35533  elmrsubrn  35722  ismfs  35751  mclsval  35765  fwddifnval  36365  weiunfrlem  36666  bj-ismoore  37437  pibp19  37750  pibp21  37751  poimirlem28  37989  cover2g  38057  seqpo  38088  incsequz2  38090  caushft  38102  ismtyval  38141  isass  38187  isexid  38188  elghomlem1OLD  38226  isrngo  38238  isrngod  38239  isgrpda  38296  rngohomval  38305  iscom2  38336  idlval  38354  pridlval  38374  maxidlval  38380  elrefrels3  38940  elcnvrefrels3  38956  eleqvrels3  39018  lflset  39525  islfld  39528  isopos  39646  isoml  39704  isatl  39765  iscvlat  39789  ishlat1  39818  psubspset  40210  lautset  40548  pautsetN  40564  ldilfset  40574  ltrnfset  40583  dilfsetN  40618  trnfsetN  40621  trnsetN  40622  trlfset  40626  tendofset  41224  tendoset  41225  dihffval  41696  lpolsetN  41948  hdmapfval  42293  hgmapfval  42352  sn-isghm  43126  aomclem8  43513  islnm  43529  clsk1independent  44497  gneispace2  44583  gneispaceel2  44595  gneispacess2  44597  caucvgbf  45941  ioodvbdlimc1lem1  46383  ioodvbdlimc1lem2  46384  ioodvbdlimc2lem  46386  issal  46766  ismea  46903  isome  46946  chnerlem1  47334  iccpartiltu  47900  iccelpart  47911  isgrim  48376  isubgrgrim  48423  isgrlim  48476  usgrexmpl2trifr  48531  gpg5nbgr3star  48575  isupwlk  48630  iscllaw  48683  iscomlaw  48684  isasslaw  48686  zlidlring  48728  uzlidlring  48729  dmatALTval  48894  islininds  48940  lindslinindsimp2  48957  ldepsnlinc  49002  elbigo  49045  iscnrm3r  49441  isprsd  49448  lubeldm2d  49451  glbeldm2d  49452  nelsubc3lem  49563  ssccatid  49565  resccatlem  49566  upciclem1  49659  upfval  49669  upfval2  49670  upfval3  49671  oppcup3lem  49699  oppcup  49700  uptr2  49714  isthincd2lem2  49928  isthincd  49929  thincpropd  49935