Theorem raleqbidv 3321

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  rspc2vd  3913  frd  5598  f12dfv  7251  f13dfv  7252  knatar  7335  ofrfvalg  7664  fmpox  8049  ovmptss  8075  frrlem4  8271  on2ind  8636  on3ind  8637  marypha1lem  9391  supeq123d  9408  oieq1  9472  acneq  10003  isfin1a  10252  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwecbv  10604  fpwwelem  10605  eltskg  10710  elgrug  10752  cau3lem  15328  rlim  15468  ello1  15488  elo1  15499  caurcvg2  15651  caucvgb  15653  fsum2dlem  15743  fsumcom2  15747  fprod2dlem  15953  fprodcom2  15957  pcfac  16877  vdwpc  16958  rami  16993  prmgaplem7  17035  prdsval  17425  ismre  17558  isacs2  17621  acsfiel  17622  iscat  17640  iscatd  17641  catidex  17642  catideu  17643  cidfval  17644  cidval  17645  catlid  17651  catrid  17652  comfeq  17674  catpropd  17677  monfval  17701  issubc  17804  fullsubc  17819  isfunc  17833  funcpropd  17871  isfull  17881  isfth  17885  fthpropd  17892  natfval  17918  initoval  17962  termoval  17963  isposd  18290  lubfval  18316  glbfval  18329  ismgm  18575  mgmpropd  18585  ismgmd  18586  issstrmgm  18587  grpidval  18595  gsumvalx  18610  gsumpropd  18612  gsumress  18616  ismgmhm  18630  resmgmhm  18645  issgrp  18654  sgrppropd  18665  ismnddef  18670  ismndd  18690  mndpropd  18693  ismhm  18719  resmhm  18754  isgrp  18878  grppropd  18890  isgrpd2e  18894  isnsg  19094  nmznsg  19107  isghm  19154  isghmOLD  19155  isga  19230  subgga  19239  gsmsymgrfix  19365  gsmsymgreq  19369  gexval  19515  ispgp  19529  isslw  19545  sylow2blem2  19558  efgval  19654  efgi  19656  efgsdm  19667  cmnpropd  19728  iscmnd  19731  submcmn2  19776  gsumzaddlem  19858  dmdprd  19937  dprdcntz  19947  isrng  20070  rngpropd  20090  issrg  20104  isring  20153  ringpropd  20204  isirred  20335  c0snmgmhm  20378  islring  20456  rrgval  20613  isdomn  20621  sdrgacs  20717  abvfval  20726  abvpropd  20751  islmod  20777  islmodd  20779  lmodprop2d  20837  lssset  20846  islmhm  20941  reslmhm  20966  lmhmpropd  20987  islbs  20990  psgndiflemA  21517  isphl  21544  islindf  21728  islindf2  21730  lsslindf  21746  isassa  21772  isassad  21781  assapropd  21788  ltbval  21957  opsrval  21960  dmatval  22386  dmatcrng  22396  scmatcrng  22415  cpmat  22603  istopg  22789  restbas  23052  ordtrest2  23098  cnfval  23127  cnpfval  23128  ist0  23214  ist1  23215  ishaus  23216  iscnrm  23217  isnrm  23229  ist0-2  23238  ishaus2  23245  nrmsep3  23249  iscmp  23282  is1stc  23335  isptfin  23410  islocfin  23411  kgenval  23429  kgencn2  23451  txbas  23461  ptval  23464  dfac14  23512  isfil  23741  isufil  23797  isufl  23807  flfcntr  23937  ucnval  24171  iscusp  24193  prdsxmslem2  24424  tngngp3  24551  isnlm  24570  nmofval  24609  lebnumii  24872  iscau4  25186  iscmet  25191  iscmet3lem1  25198  iscmet3  25200  equivcmet  25224  ulmcaulem  26310  ulmcau  26311  fsumdvdscom  27102  dchrisumlem3  27409  pntibndlem2  27509  pntibnd  27511  pntlemp  27528  ostth2lem2  27552  madebdayim  27806  no2indslem  27868  no3inds  27872  istrkgc  28388  istrkgb  28389  istrkge  28391  trgcgrg  28449  tgcgr4  28465  isismt  28468  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  uvtxval  29321  uvtxel  29322  uvtxel1  29330  uvtxusgrel  29337  cusgredg  29358  cplgr3v  29369  cplgrop  29371  usgredgsscusgredg  29394  isrgr  29494  isewlk  29537  iswlk  29545  iswwlks  29773  wlkiswwlks2  29812  isclwwlk  29920  clwlkclwwlklem1  29935  isconngr  30125  isconngr1  30126  isfrgr  30196  frgr1v  30207  nfrgr2v  30208  frgr3v  30211  1vwmgr  30212  3vfriswmgr  30214  3cyclfrgrrn1  30221  n4cyclfrgr  30227  isplig  30412  gidval  30448  vciOLD  30497  isvclem  30513  isnvlem  30546  lnoval  30688  ajfval  30745  isphg  30753  minvecolem3  30812  htth  30854  ressprs  32897  mntoval  32915  mgcoval  32919  ischn  32939  chnind  32944  chnub  32945  fxpval  33129  isslmd  33162  resv1r  33318  prmidlval  33415  mxidlval  33439  rprmval  33494  isufd  33518  constrconj  33742  iscref  33841  ordtrest2NEW  33920  fmcncfil  33928  issiga  34109  isrnsiga  34110  isldsys  34153  ismeas  34196  carsgval  34301  issibf  34331  sitgfval  34339  signstfvneq0  34570  istrkg2d  34664  ispconn  35217  issconn  35220  txpconn  35226  cvxpconn  35236  cvmscbv  35252  iscvm  35253  cvmsdisj  35264  cvmsss2  35268  snmlval  35325  elmrsubrn  35514  ismfs  35543  mclsval  35557  fwddifnval  36158  weiunfrlem  36459  bj-ismoore  37100  pibp19  37409  pibp21  37410  poimirlem28  37649  cover2g  37717  seqpo  37748  incsequz2  37750  caushft  37762  ismtyval  37801  isass  37847  isexid  37848  elghomlem1OLD  37886  isrngo  37898  isrngod  37899  isgrpda  37956  rngohomval  37965  iscom2  37996  idlval  38014  pridlval  38034  maxidlval  38040  elrefrels3  38517  elcnvrefrels3  38533  eleqvrels3  38591  lflset  39059  islfld  39062  isopos  39180  isoml  39238  isatl  39299  iscvlat  39323  ishlat1  39352  psubspset  39745  lautset  40083  pautsetN  40099  ldilfset  40109  ltrnfset  40118  dilfsetN  40153  trnfsetN  40156  trnsetN  40157  trlfset  40161  tendofset  40759  tendoset  40760  dihffval  41231  lpolsetN  41483  hdmapfval  41828  hgmapfval  41887  sn-isghm  42668  aomclem8  43057  islnm  43073  clsk1independent  44042  gneispace2  44128  gneispaceel2  44140  gneispacess2  44142  caucvgbf  45492  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  issal  46319  ismea  46456  isome  46499  iccpartiltu  47427  iccelpart  47438  isgrim  47886  isubgrgrim  47933  isgrlim  47985  usgrexmpl2trifr  48032  gpg5nbgr3star  48076  isupwlk  48128  iscllaw  48181  iscomlaw  48182  isasslaw  48184  zlidlring  48226  uzlidlring  48227  dmatALTval  48393  islininds  48439  lindslinindsimp2  48456  ldepsnlinc  48501  elbigo  48544  iscnrm3r  48940  isprsd  48947  lubeldm2d  48950  glbeldm2d  48951  nelsubc3lem  49063  ssccatid  49065  resccatlem  49066  upciclem1  49159  upfval  49169  upfval2  49170  upfval3  49171  oppcup3lem  49199  oppcup  49200  uptr2  49214  isthincd2lem2  49428  isthincd  49429  thincpropd  49435