Theorem raleqbidv 3309

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspc2vd  3899  frd  5576  f12dfv  7210  f13dfv  7211  knatar  7294  ofrfvalg  7621  fmpox  8002  ovmptss  8026  frrlem4  8222  on2ind  8587  on3ind  8588  marypha1lem  9323  supeq123d  9340  oieq1  9404  acneq  9937  isfin1a  10186  fpwwe2cbv  10524  fpwwe2lem2  10526  fpwwecbv  10538  fpwwelem  10539  eltskg  10644  elgrug  10686  cau3lem  15262  rlim  15402  ello1  15422  elo1  15433  caurcvg2  15585  caucvgb  15587  fsum2dlem  15677  fsumcom2  15681  fprod2dlem  15887  fprodcom2  15891  pcfac  16811  vdwpc  16892  rami  16927  prmgaplem7  16969  prdsval  17359  ismre  17492  isacs2  17559  acsfiel  17560  iscat  17578  iscatd  17579  catidex  17580  catideu  17581  cidfval  17582  cidval  17583  catlid  17589  catrid  17590  comfeq  17612  catpropd  17615  monfval  17639  issubc  17742  fullsubc  17757  isfunc  17771  funcpropd  17809  isfull  17819  isfth  17823  fthpropd  17830  natfval  17856  initoval  17900  termoval  17901  isposd  18228  lubfval  18254  glbfval  18267  ismgm  18515  mgmpropd  18525  ismgmd  18526  issstrmgm  18527  grpidval  18535  gsumvalx  18550  gsumpropd  18552  gsumress  18556  ismgmhm  18570  resmgmhm  18585  issgrp  18594  sgrppropd  18605  ismnddef  18610  ismndd  18630  mndpropd  18633  ismhm  18659  resmhm  18694  isgrp  18818  grppropd  18830  isgrpd2e  18834  isnsg  19034  nmznsg  19047  isghm  19094  isghmOLD  19095  isga  19170  subgga  19179  gsmsymgrfix  19307  gsmsymgreq  19311  gexval  19457  ispgp  19471  isslw  19487  sylow2blem2  19500  efgval  19596  efgi  19598  efgsdm  19609  cmnpropd  19670  iscmnd  19673  submcmn2  19718  gsumzaddlem  19800  dmdprd  19879  dprdcntz  19889  isrng  20039  rngpropd  20059  issrg  20073  isring  20122  ringpropd  20173  isirred  20304  c0snmgmhm  20347  islring  20425  rrgval  20582  isdomn  20590  sdrgacs  20686  abvfval  20695  abvpropd  20720  islmod  20767  islmodd  20769  lmodprop2d  20827  lssset  20836  islmhm  20931  reslmhm  20956  lmhmpropd  20977  islbs  20980  psgndiflemA  21508  isphl  21535  islindf  21719  islindf2  21721  lsslindf  21737  isassa  21763  isassad  21772  assapropd  21779  ltbval  21948  opsrval  21951  dmatval  22377  dmatcrng  22387  scmatcrng  22406  cpmat  22594  istopg  22780  restbas  23043  ordtrest2  23089  cnfval  23118  cnpfval  23119  ist0  23205  ist1  23206  ishaus  23207  iscnrm  23208  isnrm  23220  ist0-2  23229  ishaus2  23236  nrmsep3  23240  iscmp  23273  is1stc  23326  isptfin  23401  islocfin  23402  kgenval  23420  kgencn2  23442  txbas  23452  ptval  23455  dfac14  23503  isfil  23732  isufil  23788  isufl  23798  flfcntr  23928  ucnval  24162  iscusp  24184  prdsxmslem2  24415  tngngp3  24542  isnlm  24561  nmofval  24600  lebnumii  24863  iscau4  25177  iscmet  25182  iscmet3lem1  25189  iscmet3  25191  equivcmet  25215  ulmcaulem  26301  ulmcau  26302  fsumdvdscom  27093  dchrisumlem3  27400  pntibndlem2  27500  pntibnd  27502  pntlemp  27519  ostth2lem2  27543  madebdayim  27804  no2indslem  27868  no3inds  27872  istrkgc  28403  istrkgb  28404  istrkge  28406  trgcgrg  28464  tgcgr4  28480  isismt  28483  nbgr2vtx1edg  29299  nbuhgr2vtx1edgb  29301  uvtxval  29336  uvtxel  29337  uvtxel1  29345  uvtxusgrel  29352  cusgredg  29373  cplgr3v  29384  cplgrop  29386  usgredgsscusgredg  29409  isrgr  29509  isewlk  29552  iswlk  29560  iswwlks  29785  wlkiswwlks2  29824  isclwwlk  29932  clwlkclwwlklem1  29947  isconngr  30137  isconngr1  30138  isfrgr  30208  frgr1v  30219  nfrgr2v  30220  frgr3v  30223  1vwmgr  30224  3vfriswmgr  30226  3cyclfrgrrn1  30233  n4cyclfrgr  30239  isplig  30424  gidval  30460  vciOLD  30509  isvclem  30525  isnvlem  30558  lnoval  30700  ajfval  30757  isphg  30765  minvecolem3  30824  htth  30866  ressprs  32917  mntoval  32933  mgcoval  32937  ischn  32957  chnind  32962  chnub  32963  fxpval  33116  isslmd  33153  resv1r  33286  prmidlval  33383  mxidlval  33407  rprmval  33462  isufd  33486  constrconj  33728  iscref  33827  ordtrest2NEW  33906  fmcncfil  33914  issiga  34095  isrnsiga  34096  isldsys  34139  ismeas  34182  carsgval  34287  issibf  34317  sitgfval  34325  signstfvneq0  34556  istrkg2d  34650  ispconn  35216  issconn  35219  txpconn  35225  cvxpconn  35235  cvmscbv  35251  iscvm  35252  cvmsdisj  35263  cvmsss2  35267  snmlval  35324  elmrsubrn  35513  ismfs  35542  mclsval  35556  fwddifnval  36157  weiunfrlem  36458  bj-ismoore  37099  pibp19  37408  pibp21  37409  poimirlem28  37648  cover2g  37716  seqpo  37747  incsequz2  37749  caushft  37761  ismtyval  37800  isass  37846  isexid  37847  elghomlem1OLD  37885  isrngo  37897  isrngod  37898  isgrpda  37955  rngohomval  37964  iscom2  37995  idlval  38013  pridlval  38033  maxidlval  38039  elrefrels3  38516  elcnvrefrels3  38532  eleqvrels3  38590  lflset  39058  islfld  39061  isopos  39179  isoml  39237  isatl  39298  iscvlat  39322  ishlat1  39351  psubspset  39743  lautset  40081  pautsetN  40097  ldilfset  40107  ltrnfset  40116  dilfsetN  40151  trnfsetN  40154  trnsetN  40155  trlfset  40159  tendofset  40757  tendoset  40758  dihffval  41229  lpolsetN  41481  hdmapfval  41826  hgmapfval  41885  sn-isghm  42666  aomclem8  43054  islnm  43070  clsk1independent  44039  gneispace2  44125  gneispaceel2  44137  gneispacess2  44139  caucvgbf  45488  ioodvbdlimc1lem1  45932  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  issal  46315  ismea  46452  isome  46495  iccpartiltu  47426  iccelpart  47437  isgrim  47886  isubgrgrim  47933  isgrlim  47986  usgrexmpl2trifr  48041  gpg5nbgr3star  48085  isupwlk  48140  iscllaw  48193  iscomlaw  48194  isasslaw  48196  zlidlring  48238  uzlidlring  48239  dmatALTval  48405  islininds  48451  lindslinindsimp2  48468  ldepsnlinc  48513  elbigo  48556  iscnrm3r  48952  isprsd  48959  lubeldm2d  48962  glbeldm2d  48963  nelsubc3lem  49075  ssccatid  49077  resccatlem  49078  upciclem1  49171  upfval  49181  upfval2  49182  upfval3  49183  oppcup3lem  49211  oppcup  49212  uptr2  49226  isthincd2lem2  49440  isthincd  49441  thincpropd  49447