Theorem raleqbidv 3338

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839  df-ral 3079

This theorem is referenced by:  rspc2vd  3902  frd  5606  f12dfv  7259  f13dfv  7260  knatar  7343  ofrfvalg  7670  fmpox  8050  ovmptss  8074  frrlem4  8272  on2ind  8641  on3ind  8642  marypha1lem  9381  supeq123d  9398  oieq1  9462  acneq  10001  isfin1a  10251  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwecbv  10604  fpwwelem  10605  eltskg  10710  elgrug  10752  cau3lem  15384  rlim  15524  ello1  15544  elo1  15555  caurcvg2  15707  caucvgb  15709  fsum2dlem  15799  fsumcom2  15803  fprod2dlem  16012  fprodcom2  16016  pcfac  16937  vdwpc  17018  rami  17053  prmgaplem7  17095  prdsval  17486  ismre  17620  isacs2  17687  acsfiel  17688  iscat  17706  iscatd  17707  catidex  17708  catideu  17709  cidfval  17710  cidval  17711  catlid  17717  catrid  17718  comfeq  17740  catpropd  17743  monfval  17767  issubc  17870  fullsubc  17885  isfunc  17899  funcpropd  17937  isfull  17947  isfth  17951  fthpropd  17958  natfval  17984  initoval  18028  termoval  18029  isposd  18356  lubfval  18382  glbfval  18395  ischn  18641  chnind  18655  chnub  18656  ismgm  18677  mgmpropd  18687  ismgmd  18688  issstrmgm  18689  grpidval  18697  gsumvalx  18712  gsumpropd  18714  gsumress  18718  ismgmhm  18732  resmgmhm  18747  issgrp  18756  sgrppropd  18767  ismnddef  18772  ismndd  18792  mndpropd  18795  ismhm  18821  resmhm  18856  isgrp  18983  grppropd  18995  isgrpd2e  18999  isnsg  19198  nmznsg  19211  isghm  19258  isga  19333  subgga  19342  gsmsymgrfix  19470  gsmsymgreq  19474  gexval  19620  ispgp  19634  isslw  19650  sylow2blem2  19663  efgval  19759  efgi  19761  efgsdm  19772  cmnpropd  19833  iscmnd  19836  submcmn2  19881  gsumzaddlem  19963  dmdprd  20042  dprdcntz  20052  isrng  20202  rngpropd  20222  issrg  20240  isring  20289  ringpropd  20340  isirred  20470  c0snmgmhm  20513  islring  20592  rrgval  20749  isdomn  20757  sdrgacs  20852  abvfval  20861  abvpropd  20886  islmod  20933  islmodd  20935  lmodprop2d  20993  lssset  21002  islmhm  21096  reslmhm  21121  lmhmpropd  21142  islbs  21145  psgndiflemA  21655  isphl  21682  islindf  21866  islindf2  21868  lsslindf  21884  isassa  21910  isassad  21919  assapropd  21925  ltbval  22098  opsrval  22101  dmatval  22554  dmatcrng  22564  scmatcrng  22583  cpmat  22771  istopg  22957  restbas  23220  ordtrest2  23266  cnfval  23295  cnpfval  23296  ist0  23382  ist1  23383  ishaus  23384  iscnrm  23385  isnrm  23397  ist0-2  23406  ishaus2  23413  nrmsep3  23417  iscmp  23450  is1stc  23503  isptfin  23578  islocfin  23579  kgenval  23597  kgencn2  23619  txbas  23629  ptval  23632  dfac14  23680  isfil  23909  isufil  23965  isufl  23975  flfcntr  24105  ucnval  24338  iscusp  24360  prdsxmslem2  24591  tngngp3  24718  isnlm  24737  nmofval  24776  lebnumii  25030  iscau4  25343  iscmet  25348  iscmet3lem1  25355  iscmet3  25357  equivcmet  25381  ulmcaulem  26459  ulmcau  26460  fsumdvdscom  27251  dchrisumlem3  27557  pntibndlem2  27657  pntibnd  27659  pntlemp  27676  ostth2lem2  27700  madebdayim  27983  no2indlesm  28049  no3inds  28053  istrkgc  28625  istrkgb  28626  istrkge  28628  trgcgrg  28686  tgcgr4  28702  isismt  28705  nbgr2vtx1edg  29553  nbuhgr2vtx1edgb  29555  uvtxval  29590  uvtxel  29591  uvtxel1  29599  uvtxusgrel  29606  cusgredg  29627  cplgr3v  29638  cplgrop  29640  usgredgsscusgredg  29662  isrgr  29762  isewlk  29805  iswlk  29813  iswwlks  30038  wlkiswwlks2  30077  isclwwlk  30188  clwlkclwwlklem1  30203  isconngr  30393  isconngr1  30394  isfrgr  30464  frgr1v  30475  nfrgr2v  30476  frgr3v  30479  1vwmgr  30480  3vfriswmgr  30482  3cyclfrgrrn1  30489  n4cyclfrgr  30495  isplig  30681  gidval  30717  vciOLD  30766  isvclem  30782  isnvlem  30815  lnoval  30957  ajfval  31014  isphg  31022  minvecolem3  31081  htth  31123  ressprs  33146  mntoval  33162  mgcoval  33166  fxpval  33347  isslmd  33384  resv1r  33527  prmidlval  33625  mxidlval  33651  rprmval  33714  isufd  33738  vieta  33879  constrconj  34044  iscref  34143  ordtrest2NEW  34222  fmcncfil  34230  issiga  34411  isrnsiga  34412  isldsys  34455  ismeas  34498  carsgval  34602  issibf  34632  sitgfval  34640  signstfvneq0  34868  istrkg2d  34962  ispconn  35578  issconn  35581  txpconn  35587  cvxpconn  35597  cvmscbv  35613  iscvm  35614  cvmsdisj  35625  cvmsss2  35629  snmlval  35686  elmrsubrn  35875  ismfs  35904  mclsval  35918  fwddifnval  36518  weiunfrlem  36829  bj-ismoore  37600  pibp19  37913  pibp21  37914  poimirlem28  38152  cover2g  38220  seqpo  38251  incsequz2  38253  caushft  38265  ismtyval  38304  isass  38350  isexid  38351  elghomlem1OLD  38389  isrngo  38401  isrngod  38402  isgrpda  38459  rngohomval  38468  iscom2  38499  idlval  38517  pridlval  38537  maxidlval  38543  elrefrels3  39103  elcnvrefrels3  39119  eleqvrels3  39181  lflset  39688  islfld  39691  isopos  39809  isoml  39867  isatl  39928  iscvlat  39952  ishlat1  39981  psubspset  40373  lautset  40711  pautsetN  40727  ldilfset  40737  ltrnfset  40746  dilfsetN  40781  trnfsetN  40784  trnsetN  40785  trlfset  40789  tendofset  41387  tendoset  41388  dihffval  41859  lpolsetN  42111  hdmapfval  42456  hgmapfval  42515  sn-isghm  43260  aomclem8  43643  islnm  43659  clsk1independent  44627  gneispace2  44713  gneispaceel2  44725  gneispacess2  44727  caucvgbf  46068  ioodvbdlimc1lem1  46510  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  issal  46893  ismea  47030  isome  47073  chnerlem1  47463  iccpartiltu  48033  iccelpart  48044  isgrim  48509  isubgrgrim  48556  isgrlim  48609  usgrexmpl2trifr  48664  gpg5nbgr3star  48708  isupwlk  48763  iscllaw  48816  iscomlaw  48817  isasslaw  48819  zlidlring  48861  uzlidlring  48862  dmatALTval  49027  islininds  49073  lindslinindsimp2  49090  ldepsnlinc  49135  elbigo  49178  iscnrm3r  49574  isprsd  49581  lubeldm2d  49584  glbeldm2d  49585  nelsubc3lem  49696  ssccatid  49698  resccatlem  49699  upciclem1  49792  upfval  49802  upfval2  49803  upfval3  49804  oppcup3lem  49832  oppcup  49833  uptr2  49847  isthincd2lem2  50061  isthincd  50062  thincpropd  50068