Theorem raleqbidv 3315

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-ral 3056

This theorem is referenced by:  rspc2vd  3881  frd  5578  f12dfv  7221  f13dfv  7222  knatar  7305  ofrfvalg  7632  fmpox  8013  ovmptss  8036  frrlem4  8233  on2ind  8599  on3ind  8600  marypha1lem  9340  supeq123d  9357  oieq1  9421  acneq  9960  isfin1a  10209  fpwwe2cbv  10548  fpwwe2lem2  10550  fpwwecbv  10562  fpwwelem  10563  eltskg  10668  elgrug  10710  cau3lem  15312  rlim  15452  ello1  15472  elo1  15483  caurcvg2  15635  caucvgb  15637  fsum2dlem  15727  fsumcom2  15731  fprod2dlem  15940  fprodcom2  15944  pcfac  16865  vdwpc  16946  rami  16981  prmgaplem7  17023  prdsval  17413  ismre  17547  isacs2  17614  acsfiel  17615  iscat  17633  iscatd  17634  catidex  17635  catideu  17636  cidfval  17637  cidval  17638  catlid  17644  catrid  17645  comfeq  17667  catpropd  17670  monfval  17694  issubc  17797  fullsubc  17812  isfunc  17826  funcpropd  17864  isfull  17874  isfth  17878  fthpropd  17885  natfval  17911  initoval  17955  termoval  17956  isposd  18283  lubfval  18309  glbfval  18322  ischn  18568  chnind  18582  chnub  18583  ismgm  18604  mgmpropd  18614  ismgmd  18615  issstrmgm  18616  grpidval  18624  gsumvalx  18639  gsumpropd  18641  gsumress  18645  ismgmhm  18659  resmgmhm  18674  issgrp  18683  sgrppropd  18694  ismnddef  18699  ismndd  18719  mndpropd  18722  ismhm  18748  resmhm  18783  isgrp  18910  grppropd  18922  isgrpd2e  18926  isnsg  19125  nmznsg  19138  isghm  19185  isghmOLD  19186  isga  19261  subgga  19270  gsmsymgrfix  19398  gsmsymgreq  19402  gexval  19548  ispgp  19562  isslw  19578  sylow2blem2  19591  efgval  19687  efgi  19689  efgsdm  19700  cmnpropd  19761  iscmnd  19764  submcmn2  19809  gsumzaddlem  19891  dmdprd  19970  dprdcntz  19980  isrng  20130  rngpropd  20150  issrg  20164  isring  20213  ringpropd  20264  isirred  20394  c0snmgmhm  20437  islring  20516  rrgval  20673  isdomn  20681  sdrgacs  20777  abvfval  20786  abvpropd  20811  islmod  20858  islmodd  20860  lmodprop2d  20918  lssset  20927  islmhm  21021  reslmhm  21046  lmhmpropd  21067  islbs  21070  psgndiflemA  21580  isphl  21607  islindf  21791  islindf2  21793  lsslindf  21809  isassa  21835  isassad  21844  assapropd  21850  ltbval  22023  opsrval  22026  dmatval  22479  dmatcrng  22489  scmatcrng  22508  cpmat  22696  istopg  22882  restbas  23145  ordtrest2  23191  cnfval  23220  cnpfval  23221  ist0  23307  ist1  23308  ishaus  23309  iscnrm  23310  isnrm  23322  ist0-2  23331  ishaus2  23338  nrmsep3  23342  iscmp  23375  is1stc  23428  isptfin  23503  islocfin  23504  kgenval  23522  kgencn2  23544  txbas  23554  ptval  23557  dfac14  23605  isfil  23834  isufil  23890  isufl  23900  flfcntr  24030  ucnval  24263  iscusp  24285  prdsxmslem2  24516  tngngp3  24643  isnlm  24662  nmofval  24701  lebnumii  24955  iscau4  25268  iscmet  25273  iscmet3lem1  25280  iscmet3  25282  equivcmet  25306  ulmcaulem  26381  ulmcau  26382  fsumdvdscom  27170  dchrisumlem3  27476  pntibndlem2  27576  pntibnd  27578  pntlemp  27595  ostth2lem2  27619  madebdayim  27902  no2indlesm  27968  no3inds  27972  istrkgc  28544  istrkgb  28545  istrkge  28547  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  29550  isrgr  29650  isewlk  29693  iswlk  29701  iswwlks  29926  wlkiswwlks2  29965  isclwwlk  30076  clwlkclwwlklem1  30091  isconngr  30281  isconngr1  30282  isfrgr  30352  frgr1v  30363  nfrgr2v  30364  frgr3v  30367  1vwmgr  30368  3vfriswmgr  30370  3cyclfrgrrn1  30377  n4cyclfrgr  30383  isplig  30569  gidval  30605  vciOLD  30654  isvclem  30670  isnvlem  30703  lnoval  30845  ajfval  30902  isphg  30910  minvecolem3  30969  htth  31011  ressprs  33049  mntoval  33065  mgcoval  33069  fxpval  33250  isslmd  33287  resv1r  33426  prmidlval  33524  mxidlval  33548  rprmval  33611  isufd  33635  vieta  33776  constrconj  33941  iscref  34040  ordtrest2NEW  34119  fmcncfil  34127  issiga  34308  isrnsiga  34309  isldsys  34352  ismeas  34395  carsgval  34499  issibf  34529  sitgfval  34537  signstfvneq0  34768  istrkg2d  34862  ispconn  35466  issconn  35469  txpconn  35475  cvxpconn  35485  cvmscbv  35501  iscvm  35502  cvmsdisj  35513  cvmsss2  35517  snmlval  35574  elmrsubrn  35763  ismfs  35792  mclsval  35806  fwddifnval  36406  weiunfrlem  36707  bj-ismoore  37478  pibp19  37791  pibp21  37792  poimirlem28  38030  cover2g  38098  seqpo  38129  incsequz2  38131  caushft  38143  ismtyval  38182  isass  38228  isexid  38229  elghomlem1OLD  38267  isrngo  38279  isrngod  38280  isgrpda  38337  rngohomval  38346  iscom2  38377  idlval  38395  pridlval  38415  maxidlval  38421  elrefrels3  38981  elcnvrefrels3  38997  eleqvrels3  39059  lflset  39566  islfld  39569  isopos  39687  isoml  39745  isatl  39806  iscvlat  39830  ishlat1  39859  psubspset  40251  lautset  40589  pautsetN  40605  ldilfset  40615  ltrnfset  40624  dilfsetN  40659  trnfsetN  40662  trnsetN  40663  trlfset  40667  tendofset  41265  tendoset  41266  dihffval  41737  lpolsetN  41989  hdmapfval  42334  hgmapfval  42393  sn-isghm  43138  aomclem8  43521  islnm  43537  clsk1independent  44505  gneispace2  44591  gneispaceel2  44603  gneispacess2  44605  caucvgbf  45946  ioodvbdlimc1lem1  46388  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  issal  46771  ismea  46908  isome  46951  chnerlem1  47341  iccpartiltu  47911  iccelpart  47922  isgrim  48387  isubgrgrim  48434  isgrlim  48487  usgrexmpl2trifr  48542  gpg5nbgr3star  48586  isupwlk  48641  iscllaw  48694  iscomlaw  48695  isasslaw  48697  zlidlring  48739  uzlidlring  48740  dmatALTval  48905  islininds  48951  lindslinindsimp2  48968  ldepsnlinc  49013  elbigo  49056  iscnrm3r  49452  isprsd  49459  lubeldm2d  49462  glbeldm2d  49463  nelsubc3lem  49574  ssccatid  49576  resccatlem  49577  upciclem1  49670  upfval  49680  upfval2  49681  upfval3  49682  oppcup3lem  49710  oppcup  49711  uptr2  49725  isthincd2lem2  49939  isthincd  49940  thincpropd  49946