Theorem raleqbidv 3327

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-ral 3068

This theorem is referenced by:  rspc2vd  3879  frd  5539  f12dfv  7126  f13dfv  7127  knatar  7208  ofrfvalg  7519  fmpox  7880  ovmptss  7904  frrlem4  8076  marypha1lem  9122  supeq123d  9139  oieq1  9201  acneq  9730  isfin1a  9979  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwecbv  10331  fpwwelem  10332  eltskg  10437  elgrug  10479  cau3lem  14994  rlim  15132  ello1  15152  elo1  15163  caurcvg2  15317  caucvgb  15319  fsum2dlem  15410  fsumcom2  15414  fprod2dlem  15618  fprodcom2  15622  pcfac  16528  vdwpc  16609  rami  16644  prmgaplem7  16686  prdsval  17083  ismre  17216  isacs2  17279  acsfiel  17280  iscat  17298  iscatd  17299  catidex  17300  catideu  17301  cidfval  17302  cidval  17303  catlid  17309  catrid  17310  comfeq  17332  catpropd  17335  monfval  17361  issubc  17466  fullsubc  17481  isfunc  17495  funcpropd  17532  isfull  17542  isfth  17546  fthpropd  17553  natfval  17578  initoval  17624  termoval  17625  isposd  17956  lubfval  17983  glbfval  17996  ismgm  18242  issstrmgm  18252  grpidval  18260  gsumvalx  18275  gsumpropd  18277  gsumress  18281  issgrp  18291  ismnddef  18302  ismndd  18322  mndpropd  18325  ismhm  18347  resmhm  18374  isgrp  18498  grppropd  18509  isgrpd2e  18513  isnsg  18698  nmznsg  18711  isghm  18749  isga  18812  subgga  18821  gsmsymgrfix  18951  gsmsymgreq  18955  gexval  19098  ispgp  19112  isslw  19128  sylow2blem2  19141  efgval  19238  efgi  19240  efgsdm  19251  cmnpropd  19311  iscmnd  19314  submcmn2  19355  gsumzaddlem  19437  dmdprd  19516  dprdcntz  19526  issrg  19658  isring  19702  ringpropd  19736  isirred  19856  sdrgacs  19984  abvfval  19993  abvpropd  20017  islmod  20042  islmodd  20044  lmodprop2d  20100  lssset  20110  islmhm  20204  reslmhm  20229  lmhmpropd  20250  islbs  20253  rrgval  20471  isdomn  20478  psgndiflemA  20718  isphl  20745  islindf  20929  islindf2  20931  lsslindf  20947  isassa  20973  isassad  20981  assapropd  20986  ltbval  21154  opsrval  21157  dmatval  21549  dmatcrng  21559  scmatcrng  21578  cpmat  21766  istopg  21952  restbas  22217  ordtrest2  22263  cnfval  22292  cnpfval  22293  ist0  22379  ist1  22380  ishaus  22381  iscnrm  22382  isnrm  22394  ist0-2  22403  ishaus2  22410  nrmsep3  22414  iscmp  22447  is1stc  22500  isptfin  22575  islocfin  22576  kgenval  22594  kgencn2  22616  txbas  22626  ptval  22629  dfac14  22677  isfil  22906  isufil  22962  isufl  22972  flfcntr  23102  ucnval  23337  iscusp  23359  prdsxmslem2  23591  tngngp3  23726  isnlm  23745  nmofval  23784  lebnumii  24035  iscau4  24348  iscmet  24353  iscmet3lem1  24360  iscmet3  24362  equivcmet  24386  ulmcaulem  25458  ulmcau  25459  fsumdvdscom  26239  dchrisumlem3  26544  pntibndlem2  26644  pntibnd  26646  pntlemp  26663  ostth2lem2  26687  trgcgrg  26780  tgcgr4  26796  isismt  26799  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  uvtxval  27657  uvtxel  27658  uvtxel1  27666  uvtxusgrel  27673  cusgredg  27694  cplgr3v  27705  cplgrop  27707  usgredgsscusgredg  27729  isrgr  27829  isewlk  27872  iswlk  27880  iswwlks  28102  wlkiswwlks2  28141  isclwwlk  28249  clwlkclwwlklem1  28264  isconngr  28454  isconngr1  28455  isfrgr  28525  frgr1v  28536  nfrgr2v  28537  frgr3v  28540  1vwmgr  28541  3vfriswmgr  28543  3cyclfrgrrn1  28550  n4cyclfrgr  28556  isplig  28739  gidval  28775  vciOLD  28824  isvclem  28840  isnvlem  28873  lnoval  29015  ajfval  29072  isphg  29080  minvecolem3  29139  htth  29181  ressprs  31143  mntoval  31162  mgcoval  31166  isslmd  31357  resv1r  31443  prmidlval  31514  mxidlval  31535  isufd  31565  rprmval  31566  iscref  31696  ordtrest2NEW  31775  fmcncfil  31783  issiga  31980  isrnsiga  31981  isldsys  32024  ismeas  32067  carsgval  32170  issibf  32200  sitgfval  32208  signstfvneq0  32451  istrkg2d  32546  ispconn  33085  issconn  33088  txpconn  33094  cvxpconn  33104  cvmscbv  33120  iscvm  33121  cvmsdisj  33132  cvmsss2  33136  snmlval  33193  elmrsubrn  33382  ismfs  33411  mclsval  33425  on2ind  33755  on3ind  33756  madebdayim  33997  no2indslem  34038  no3inds  34042  fwddifnval  34392  bj-ismoore  35203  pibp19  35512  pibp21  35513  poimirlem28  35732  cover2g  35800  seqpo  35832  incsequz2  35834  caushft  35846  ismtyval  35885  isass  35931  isexid  35932  elghomlem1OLD  35970  isrngo  35982  isrngod  35983  isgrpda  36040  rngohomval  36049  iscom2  36080  idlval  36098  pridlval  36118  maxidlval  36124  elrefrels3  36563  elcnvrefrels3  36576  eleqvrels3  36633  lflset  37000  islfld  37003  isopos  37121  isoml  37179  isatl  37240  iscvlat  37264  ishlat1  37293  psubspset  37685  lautset  38023  pautsetN  38039  ldilfset  38049  ltrnfset  38058  dilfsetN  38093  trnfsetN  38096  trnsetN  38097  trlfset  38101  tendofset  38699  tendoset  38700  dihffval  39171  lpolsetN  39423  hdmapfval  39768  hgmapfval  39827  aomclem8  40802  islnm  40818  clsk1independent  41545  gneispace2  41631  gneispaceel2  41643  gneispacess2  41645  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  issal  43745  ismea  43879  isome  43922  iccpartiltu  44762  iccelpart  44773  isomgr  45163  isupwlk  45186  mgmpropd  45217  ismgmd  45218  ismgmhm  45225  resmgmhm  45240  iscllaw  45271  iscomlaw  45272  isasslaw  45274  isrng  45322  c0snmgmhm  45360  zlidlring  45374  uzlidlring  45375  dmatALTval  45629  islininds  45675  lindslinindsimp2  45692  ldepsnlinc  45737  elbigo  45785  iscnrm3r  46130  isprsd  46137  lubeldm2d  46140  glbeldm2d  46141  isthincd2lem2  46205  isthincd  46206