Theorem raleqbidv 3318

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  3899  frd  5591  f12dfv  7231  f13dfv  7232  knatar  7315  ofrfvalg  7642  fmpox  8023  ovmptss  8047  frrlem4  8243  on2ind  8609  on3ind  8610  marypha1lem  9350  supeq123d  9367  oieq1  9431  acneq  9967  isfin1a  10216  fpwwe2cbv  10555  fpwwe2lem2  10557  fpwwecbv  10569  fpwwelem  10570  eltskg  10675  elgrug  10717  cau3lem  15292  rlim  15432  ello1  15452  elo1  15463  caurcvg2  15615  caucvgb  15617  fsum2dlem  15707  fsumcom2  15711  fprod2dlem  15917  fprodcom2  15921  pcfac  16841  vdwpc  16922  rami  16957  prmgaplem7  16999  prdsval  17389  ismre  17523  isacs2  17590  acsfiel  17591  iscat  17609  iscatd  17610  catidex  17611  catideu  17612  cidfval  17613  cidval  17614  catlid  17620  catrid  17621  comfeq  17643  catpropd  17646  monfval  17670  issubc  17773  fullsubc  17788  isfunc  17802  funcpropd  17840  isfull  17850  isfth  17854  fthpropd  17861  natfval  17887  initoval  17931  termoval  17932  isposd  18259  lubfval  18285  glbfval  18298  ischn  18544  chnind  18558  chnub  18559  ismgm  18580  mgmpropd  18590  ismgmd  18591  issstrmgm  18592  grpidval  18600  gsumvalx  18615  gsumpropd  18617  gsumress  18621  ismgmhm  18635  resmgmhm  18650  issgrp  18659  sgrppropd  18670  ismnddef  18675  ismndd  18695  mndpropd  18698  ismhm  18724  resmhm  18759  isgrp  18886  grppropd  18898  isgrpd2e  18902  isnsg  19101  nmznsg  19114  isghm  19161  isghmOLD  19162  isga  19237  subgga  19246  gsmsymgrfix  19374  gsmsymgreq  19378  gexval  19524  ispgp  19538  isslw  19554  sylow2blem2  19567  efgval  19663  efgi  19665  efgsdm  19676  cmnpropd  19737  iscmnd  19740  submcmn2  19785  gsumzaddlem  19867  dmdprd  19946  dprdcntz  19956  isrng  20106  rngpropd  20126  issrg  20140  isring  20189  ringpropd  20240  isirred  20372  c0snmgmhm  20415  islring  20490  rrgval  20647  isdomn  20655  sdrgacs  20751  abvfval  20760  abvpropd  20785  islmod  20832  islmodd  20834  lmodprop2d  20892  lssset  20901  islmhm  20996  reslmhm  21021  lmhmpropd  21042  islbs  21045  psgndiflemA  21573  isphl  21600  islindf  21784  islindf2  21786  lsslindf  21802  isassa  21828  isassad  21837  assapropd  21844  ltbval  22015  opsrval  22018  dmatval  22453  dmatcrng  22463  scmatcrng  22482  cpmat  22670  istopg  22856  restbas  23119  ordtrest2  23165  cnfval  23194  cnpfval  23195  ist0  23281  ist1  23282  ishaus  23283  iscnrm  23284  isnrm  23296  ist0-2  23305  ishaus2  23312  nrmsep3  23316  iscmp  23349  is1stc  23402  isptfin  23477  islocfin  23478  kgenval  23496  kgencn2  23518  txbas  23528  ptval  23531  dfac14  23579  isfil  23808  isufil  23864  isufl  23874  flfcntr  24004  ucnval  24237  iscusp  24259  prdsxmslem2  24490  tngngp3  24617  isnlm  24636  nmofval  24675  lebnumii  24938  iscau4  25252  iscmet  25257  iscmet3lem1  25264  iscmet3  25266  equivcmet  25290  ulmcaulem  26376  ulmcau  26377  fsumdvdscom  27168  dchrisumlem3  27475  pntibndlem2  27575  pntibnd  27577  pntlemp  27594  ostth2lem2  27618  madebdayim  27901  no2indlesm  27967  no3inds  27971  istrkgc  28543  istrkgb  28544  istrkge  28546  trgcgrg  28605  tgcgr4  28621  isismt  28624  nbgr2vtx1edg  29441  nbuhgr2vtx1edgb  29443  uvtxval  29478  uvtxel  29479  uvtxel1  29487  uvtxusgrel  29494  cusgredg  29515  cplgr3v  29526  cplgrop  29528  usgredgsscusgredg  29551  isrgr  29651  isewlk  29694  iswlk  29702  iswwlks  29927  wlkiswwlks2  29966  isclwwlk  30077  clwlkclwwlklem1  30092  isconngr  30282  isconngr1  30283  isfrgr  30353  frgr1v  30364  nfrgr2v  30365  frgr3v  30368  1vwmgr  30369  3vfriswmgr  30371  3cyclfrgrrn1  30378  n4cyclfrgr  30384  isplig  30570  gidval  30606  vciOLD  30655  isvclem  30671  isnvlem  30704  lnoval  30846  ajfval  30903  isphg  30911  minvecolem3  30970  htth  31012  ressprs  33065  mntoval  33081  mgcoval  33085  fxpval  33265  isslmd  33302  resv1r  33438  prmidlval  33536  mxidlval  33560  rprmval  33615  isufd  33639  vieta  33763  constrconj  33929  iscref  34028  ordtrest2NEW  34107  fmcncfil  34115  issiga  34296  isrnsiga  34297  isldsys  34340  ismeas  34383  carsgval  34487  issibf  34517  sitgfval  34525  signstfvneq0  34756  istrkg2d  34850  ispconn  35445  issconn  35448  txpconn  35454  cvxpconn  35464  cvmscbv  35480  iscvm  35481  cvmsdisj  35492  cvmsss2  35496  snmlval  35553  elmrsubrn  35742  ismfs  35771  mclsval  35785  fwddifnval  36385  weiunfrlem  36686  bj-ismoore  37385  pibp19  37696  pibp21  37697  poimirlem28  37928  cover2g  37996  seqpo  38027  incsequz2  38029  caushft  38041  ismtyval  38080  isass  38126  isexid  38127  elghomlem1OLD  38165  isrngo  38177  isrngod  38178  isgrpda  38235  rngohomval  38244  iscom2  38275  idlval  38293  pridlval  38313  maxidlval  38319  elrefrels3  38879  elcnvrefrels3  38895  eleqvrels3  38957  lflset  39464  islfld  39467  isopos  39585  isoml  39643  isatl  39704  iscvlat  39728  ishlat1  39757  psubspset  40149  lautset  40487  pautsetN  40503  ldilfset  40513  ltrnfset  40522  dilfsetN  40557  trnfsetN  40560  trnsetN  40561  trlfset  40565  tendofset  41163  tendoset  41164  dihffval  41635  lpolsetN  41887  hdmapfval  42232  hgmapfval  42291  sn-isghm  43060  aomclem8  43447  islnm  43463  clsk1independent  44431  gneispace2  44517  gneispaceel2  44529  gneispacess2  44531  caucvgbf  45876  ioodvbdlimc1lem1  46318  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  issal  46701  ismea  46838  isome  46881  chnerlem1  47269  iccpartiltu  47811  iccelpart  47822  isgrim  48271  isubgrgrim  48318  isgrlim  48371  usgrexmpl2trifr  48426  gpg5nbgr3star  48470  isupwlk  48525  iscllaw  48578  iscomlaw  48579  isasslaw  48581  zlidlring  48623  uzlidlring  48624  dmatALTval  48789  islininds  48835  lindslinindsimp2  48852  ldepsnlinc  48897  elbigo  48940  iscnrm3r  49336  isprsd  49343  lubeldm2d  49346  glbeldm2d  49347  nelsubc3lem  49458  ssccatid  49460  resccatlem  49461  upciclem1  49554  upfval  49564  upfval2  49565  upfval3  49566  oppcup3lem  49594  oppcup  49595  uptr2  49609  isthincd2lem2  49823  isthincd  49824  thincpropd  49830