Theorem raleqbidv 3317

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 3156	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  3898  frd  5582  f12dfv  7221  f13dfv  7222  knatar  7305  ofrfvalg  7632  fmpox  8013  ovmptss  8037  frrlem4  8233  on2ind  8599  on3ind  8600  marypha1lem  9340  supeq123d  9357  oieq1  9421  acneq  9957  isfin1a  10206  fpwwe2cbv  10545  fpwwe2lem2  10547  fpwwecbv  10559  fpwwelem  10560  eltskg  10665  elgrug  10707  cau3lem  15282  rlim  15422  ello1  15442  elo1  15453  caurcvg2  15605  caucvgb  15607  fsum2dlem  15697  fsumcom2  15701  fprod2dlem  15907  fprodcom2  15911  pcfac  16831  vdwpc  16912  rami  16947  prmgaplem7  16989  prdsval  17379  ismre  17513  isacs2  17580  acsfiel  17581  iscat  17599  iscatd  17600  catidex  17601  catideu  17602  cidfval  17603  cidval  17604  catlid  17610  catrid  17611  comfeq  17633  catpropd  17636  monfval  17660  issubc  17763  fullsubc  17778  isfunc  17792  funcpropd  17830  isfull  17840  isfth  17844  fthpropd  17851  natfval  17877  initoval  17921  termoval  17922  isposd  18249  lubfval  18275  glbfval  18288  ischn  18534  chnind  18548  chnub  18549  ismgm  18570  mgmpropd  18580  ismgmd  18581  issstrmgm  18582  grpidval  18590  gsumvalx  18605  gsumpropd  18607  gsumress  18611  ismgmhm  18625  resmgmhm  18640  issgrp  18649  sgrppropd  18660  ismnddef  18665  ismndd  18685  mndpropd  18688  ismhm  18714  resmhm  18749  isgrp  18873  grppropd  18885  isgrpd2e  18889  isnsg  19088  nmznsg  19101  isghm  19148  isghmOLD  19149  isga  19224  subgga  19233  gsmsymgrfix  19361  gsmsymgreq  19365  gexval  19511  ispgp  19525  isslw  19541  sylow2blem2  19554  efgval  19650  efgi  19652  efgsdm  19663  cmnpropd  19724  iscmnd  19727  submcmn2  19772  gsumzaddlem  19854  dmdprd  19933  dprdcntz  19943  isrng  20093  rngpropd  20113  issrg  20127  isring  20176  ringpropd  20227  isirred  20359  c0snmgmhm  20402  islring  20477  rrgval  20634  isdomn  20642  sdrgacs  20738  abvfval  20747  abvpropd  20772  islmod  20819  islmodd  20821  lmodprop2d  20879  lssset  20888  islmhm  20983  reslmhm  21008  lmhmpropd  21029  islbs  21032  psgndiflemA  21560  isphl  21587  islindf  21771  islindf2  21773  lsslindf  21789  isassa  21815  isassad  21824  assapropd  21831  ltbval  22002  opsrval  22005  dmatval  22440  dmatcrng  22450  scmatcrng  22469  cpmat  22657  istopg  22843  restbas  23106  ordtrest2  23152  cnfval  23181  cnpfval  23182  ist0  23268  ist1  23269  ishaus  23270  iscnrm  23271  isnrm  23283  ist0-2  23292  ishaus2  23299  nrmsep3  23303  iscmp  23336  is1stc  23389  isptfin  23464  islocfin  23465  kgenval  23483  kgencn2  23505  txbas  23515  ptval  23518  dfac14  23566  isfil  23795  isufil  23851  isufl  23861  flfcntr  23991  ucnval  24224  iscusp  24246  prdsxmslem2  24477  tngngp3  24604  isnlm  24623  nmofval  24662  lebnumii  24925  iscau4  25239  iscmet  25244  iscmet3lem1  25251  iscmet3  25253  equivcmet  25277  ulmcaulem  26363  ulmcau  26364  fsumdvdscom  27155  dchrisumlem3  27462  pntibndlem2  27562  pntibnd  27564  pntlemp  27581  ostth2lem2  27605  madebdayim  27888  no2indlesm  27954  no3inds  27958  istrkgc  28530  istrkgb  28531  istrkge  28533  trgcgrg  28591  tgcgr4  28607  isismt  28610  nbgr2vtx1edg  29427  nbuhgr2vtx1edgb  29429  uvtxval  29464  uvtxel  29465  uvtxel1  29473  uvtxusgrel  29480  cusgredg  29501  cplgr3v  29512  cplgrop  29514  usgredgsscusgredg  29537  isrgr  29637  isewlk  29680  iswlk  29688  iswwlks  29913  wlkiswwlks2  29952  isclwwlk  30063  clwlkclwwlklem1  30078  isconngr  30268  isconngr1  30269  isfrgr  30339  frgr1v  30350  nfrgr2v  30351  frgr3v  30354  1vwmgr  30355  3vfriswmgr  30357  3cyclfrgrrn1  30364  n4cyclfrgr  30370  isplig  30555  gidval  30591  vciOLD  30640  isvclem  30656  isnvlem  30689  lnoval  30831  ajfval  30888  isphg  30896  minvecolem3  30955  htth  30997  ressprs  33050  mntoval  33066  mgcoval  33070  fxpval  33249  isslmd  33286  resv1r  33422  prmidlval  33520  mxidlval  33544  rprmval  33599  isufd  33623  vieta  33738  constrconj  33904  iscref  34003  ordtrest2NEW  34082  fmcncfil  34090  issiga  34271  isrnsiga  34272  isldsys  34315  ismeas  34358  carsgval  34462  issibf  34492  sitgfval  34500  signstfvneq0  34731  istrkg2d  34825  ispconn  35419  issconn  35422  txpconn  35428  cvxpconn  35438  cvmscbv  35454  iscvm  35455  cvmsdisj  35466  cvmsss2  35470  snmlval  35527  elmrsubrn  35716  ismfs  35745  mclsval  35759  fwddifnval  36359  weiunfrlem  36660  bj-ismoore  37312  pibp19  37621  pibp21  37622  poimirlem28  37851  cover2g  37919  seqpo  37950  incsequz2  37952  caushft  37964  ismtyval  38003  isass  38049  isexid  38050  elghomlem1OLD  38088  isrngo  38100  isrngod  38101  isgrpda  38158  rngohomval  38167  iscom2  38198  idlval  38216  pridlval  38236  maxidlval  38242  elrefrels3  38802  elcnvrefrels3  38818  eleqvrels3  38880  lflset  39387  islfld  39390  isopos  39508  isoml  39566  isatl  39627  iscvlat  39651  ishlat1  39680  psubspset  40072  lautset  40410  pautsetN  40426  ldilfset  40436  ltrnfset  40445  dilfsetN  40480  trnfsetN  40483  trnsetN  40484  trlfset  40488  tendofset  41086  tendoset  41087  dihffval  41558  lpolsetN  41810  hdmapfval  42155  hgmapfval  42214  sn-isghm  42983  aomclem8  43370  islnm  43386  clsk1independent  44354  gneispace2  44440  gneispaceel2  44452  gneispacess2  44454  caucvgbf  45800  ioodvbdlimc1lem1  46242  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  issal  46625  ismea  46762  isome  46805  chnerlem1  47193  iccpartiltu  47735  iccelpart  47746  isgrim  48195  isubgrgrim  48242  isgrlim  48295  usgrexmpl2trifr  48350  gpg5nbgr3star  48394  isupwlk  48449  iscllaw  48502  iscomlaw  48503  isasslaw  48505  zlidlring  48547  uzlidlring  48548  dmatALTval  48713  islininds  48759  lindslinindsimp2  48776  ldepsnlinc  48821  elbigo  48864  iscnrm3r  49260  isprsd  49267  lubeldm2d  49270  glbeldm2d  49271  nelsubc3lem  49382  ssccatid  49384  resccatlem  49385  upciclem1  49478  upfval  49488  upfval2  49489  upfval3  49490  oppcup3lem  49518  oppcup  49519  uptr2  49533  isthincd2lem2  49747  isthincd  49748  thincpropd  49754