Theorem raleqbidv 3311

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspc2vd  3885  frd  5588  f12dfv  7228  f13dfv  7229  knatar  7312  ofrfvalg  7639  fmpox  8020  ovmptss  8043  frrlem4  8239  on2ind  8605  on3ind  8606  marypha1lem  9346  supeq123d  9363  oieq1  9427  acneq  9965  isfin1a  10214  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwecbv  10567  fpwwelem  10568  eltskg  10673  elgrug  10715  cau3lem  15317  rlim  15457  ello1  15477  elo1  15488  caurcvg2  15640  caucvgb  15642  fsum2dlem  15732  fsumcom2  15736  fprod2dlem  15945  fprodcom2  15949  pcfac  16870  vdwpc  16951  rami  16986  prmgaplem7  17028  prdsval  17418  ismre  17552  isacs2  17619  acsfiel  17620  iscat  17638  iscatd  17639  catidex  17640  catideu  17641  cidfval  17642  cidval  17643  catlid  17649  catrid  17650  comfeq  17672  catpropd  17675  monfval  17699  issubc  17802  fullsubc  17817  isfunc  17831  funcpropd  17869  isfull  17879  isfth  17883  fthpropd  17890  natfval  17916  initoval  17960  termoval  17961  isposd  18288  lubfval  18314  glbfval  18327  ischn  18573  chnind  18587  chnub  18588  ismgm  18609  mgmpropd  18619  ismgmd  18620  issstrmgm  18621  grpidval  18629  gsumvalx  18644  gsumpropd  18646  gsumress  18650  ismgmhm  18664  resmgmhm  18679  issgrp  18688  sgrppropd  18699  ismnddef  18704  ismndd  18724  mndpropd  18727  ismhm  18753  resmhm  18788  isgrp  18915  grppropd  18927  isgrpd2e  18931  isnsg  19130  nmznsg  19143  isghm  19190  isghmOLD  19191  isga  19266  subgga  19275  gsmsymgrfix  19403  gsmsymgreq  19407  gexval  19553  ispgp  19567  isslw  19583  sylow2blem2  19596  efgval  19692  efgi  19694  efgsdm  19705  cmnpropd  19766  iscmnd  19769  submcmn2  19814  gsumzaddlem  19896  dmdprd  19975  dprdcntz  19985  isrng  20135  rngpropd  20155  issrg  20169  isring  20218  ringpropd  20269  isirred  20399  c0snmgmhm  20442  islring  20517  rrgval  20674  isdomn  20682  sdrgacs  20778  abvfval  20787  abvpropd  20812  islmod  20859  islmodd  20861  lmodprop2d  20919  lssset  20928  islmhm  21022  reslmhm  21047  lmhmpropd  21068  islbs  21071  psgndiflemA  21581  isphl  21608  islindf  21792  islindf2  21794  lsslindf  21810  isassa  21836  isassad  21845  assapropd  21851  ltbval  22021  opsrval  22024  dmatval  22457  dmatcrng  22467  scmatcrng  22486  cpmat  22674  istopg  22860  restbas  23123  ordtrest2  23169  cnfval  23198  cnpfval  23199  ist0  23285  ist1  23286  ishaus  23287  iscnrm  23288  isnrm  23300  ist0-2  23309  ishaus2  23316  nrmsep3  23320  iscmp  23353  is1stc  23406  isptfin  23481  islocfin  23482  kgenval  23500  kgencn2  23522  txbas  23532  ptval  23535  dfac14  23583  isfil  23812  isufil  23868  isufl  23878  flfcntr  24008  ucnval  24241  iscusp  24263  prdsxmslem2  24494  tngngp3  24621  isnlm  24640  nmofval  24679  lebnumii  24933  iscau4  25246  iscmet  25251  iscmet3lem1  25258  iscmet3  25260  equivcmet  25284  ulmcaulem  26359  ulmcau  26360  fsumdvdscom  27148  dchrisumlem3  27454  pntibndlem2  27554  pntibnd  27556  pntlemp  27573  ostth2lem2  27597  madebdayim  27880  no2indlesm  27946  no3inds  27950  istrkgc  28522  istrkgb  28523  istrkge  28525  trgcgrg  28583  tgcgr4  28599  isismt  28602  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  uvtxval  29456  uvtxel  29457  uvtxel1  29465  uvtxusgrel  29472  cusgredg  29493  cplgr3v  29504  cplgrop  29506  usgredgsscusgredg  29528  isrgr  29628  isewlk  29671  iswlk  29679  iswwlks  29904  wlkiswwlks2  29943  isclwwlk  30054  clwlkclwwlklem1  30069  isconngr  30259  isconngr1  30260  isfrgr  30330  frgr1v  30341  nfrgr2v  30342  frgr3v  30345  1vwmgr  30346  3vfriswmgr  30348  3cyclfrgrrn1  30355  n4cyclfrgr  30361  isplig  30547  gidval  30583  vciOLD  30632  isvclem  30648  isnvlem  30681  lnoval  30823  ajfval  30880  isphg  30888  minvecolem3  30947  htth  30989  ressprs  33026  mntoval  33042  mgcoval  33046  fxpval  33226  isslmd  33263  resv1r  33399  prmidlval  33497  mxidlval  33521  rprmval  33576  isufd  33600  vieta  33724  constrconj  33889  iscref  33988  ordtrest2NEW  34067  fmcncfil  34075  issiga  34256  isrnsiga  34257  isldsys  34300  ismeas  34343  carsgval  34447  issibf  34477  sitgfval  34485  signstfvneq0  34716  istrkg2d  34810  ispconn  35405  issconn  35408  txpconn  35414  cvxpconn  35424  cvmscbv  35440  iscvm  35441  cvmsdisj  35452  cvmsss2  35456  snmlval  35513  elmrsubrn  35702  ismfs  35731  mclsval  35745  fwddifnval  36345  weiunfrlem  36646  bj-ismoore  37417  pibp19  37730  pibp21  37731  poimirlem28  37969  cover2g  38037  seqpo  38068  incsequz2  38070  caushft  38082  ismtyval  38121  isass  38167  isexid  38168  elghomlem1OLD  38206  isrngo  38218  isrngod  38219  isgrpda  38276  rngohomval  38285  iscom2  38316  idlval  38334  pridlval  38354  maxidlval  38360  elrefrels3  38920  elcnvrefrels3  38936  eleqvrels3  38998  lflset  39505  islfld  39508  isopos  39626  isoml  39684  isatl  39745  iscvlat  39769  ishlat1  39798  psubspset  40190  lautset  40528  pautsetN  40544  ldilfset  40554  ltrnfset  40563  dilfsetN  40598  trnfsetN  40601  trnsetN  40602  trlfset  40606  tendofset  41204  tendoset  41205  dihffval  41676  lpolsetN  41928  hdmapfval  42273  hgmapfval  42332  sn-isghm  43106  aomclem8  43489  islnm  43505  clsk1independent  44473  gneispace2  44559  gneispaceel2  44571  gneispacess2  44573  caucvgbf  45917  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  issal  46742  ismea  46879  isome  46922  chnerlem1  47312  iccpartiltu  47882  iccelpart  47893  isgrim  48358  isubgrgrim  48405  isgrlim  48458  usgrexmpl2trifr  48513  gpg5nbgr3star  48557  isupwlk  48612  iscllaw  48665  iscomlaw  48666  isasslaw  48668  zlidlring  48710  uzlidlring  48711  dmatALTval  48876  islininds  48922  lindslinindsimp2  48939  ldepsnlinc  48984  elbigo  49027  iscnrm3r  49423  isprsd  49430  lubeldm2d  49433  glbeldm2d  49434  nelsubc3lem  49545  ssccatid  49547  resccatlem  49548  upciclem1  49641  upfval  49651  upfval2  49652  upfval3  49653  oppcup3lem  49681  oppcup  49682  uptr2  49696  isthincd2lem2  49910  isthincd  49911  thincpropd  49917