Theorem raleqbidv 3306

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2110  ∀wral 3054

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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2726  df-clel 2812  df-ral 3059

This theorem is referenced by:  rspc2vd  3853  f12dfv  7073  f13dfv  7074  knatar  7155  ofrfvalg  7465  fmpox  7826  ovmptss  7850  frrlem4  8019  marypha1lem  9038  supeq123d  9055  oieq1  9117  acneq  9640  isfin1a  9889  fpwwe2cbv  10227  fpwwe2lem2  10229  fpwwecbv  10241  fpwwelem  10242  eltskg  10347  elgrug  10389  cau3lem  14901  rlim  15039  ello1  15059  elo1  15070  caurcvg2  15224  caucvgb  15226  fsum2dlem  15315  fsumcom2  15319  fprod2dlem  15523  fprodcom2  15527  pcfac  16433  vdwpc  16514  rami  16549  prmgaplem7  16591  prdsval  16932  ismre  17065  isacs2  17128  acsfiel  17129  iscat  17147  iscatd  17148  catidex  17149  catideu  17150  cidfval  17151  cidval  17152  catlid  17158  catrid  17159  comfeq  17181  catpropd  17184  monfval  17209  issubc  17313  fullsubc  17328  isfunc  17342  funcpropd  17379  isfull  17389  isfth  17393  fthpropd  17400  natfval  17425  initoval  17471  termoval  17472  isposd  17802  lubfval  17828  glbfval  17841  ismgm  18087  issstrmgm  18097  grpidval  18105  gsumvalx  18120  gsumpropd  18122  gsumress  18126  issgrp  18136  ismnddef  18147  ismndd  18167  mndpropd  18170  ismhm  18192  resmhm  18219  isgrp  18343  grppropd  18354  isgrpd2e  18358  isnsg  18543  nmznsg  18556  isghm  18594  isga  18657  subgga  18666  gsmsymgrfix  18792  gsmsymgreq  18796  gexval  18939  ispgp  18953  isslw  18969  sylow2blem2  18982  efgval  19079  efgi  19081  efgsdm  19092  cmnpropd  19152  iscmnd  19155  submcmn2  19196  gsumzaddlem  19278  dmdprd  19357  dprdcntz  19367  issrg  19494  isring  19538  ringpropd  19572  isirred  19689  sdrgacs  19817  abvfval  19826  abvpropd  19850  islmod  19875  islmodd  19877  lmodprop2d  19933  lssset  19942  islmhm  20036  reslmhm  20061  lmhmpropd  20082  islbs  20085  rrgval  20297  isdomn  20304  psgndiflemA  20535  isphl  20562  islindf  20746  islindf2  20748  lsslindf  20764  isassa  20790  isassad  20798  assapropd  20803  ltbval  20972  opsrval  20975  dmatval  21361  dmatcrng  21371  scmatcrng  21390  cpmat  21578  istopg  21764  restbas  22027  ordtrest2  22073  cnfval  22102  cnpfval  22103  ist0  22189  ist1  22190  ishaus  22191  iscnrm  22192  isnrm  22204  ist0-2  22213  ishaus2  22220  nrmsep3  22224  iscmp  22257  is1stc  22310  isptfin  22385  islocfin  22386  kgenval  22404  kgencn2  22426  txbas  22436  ptval  22439  dfac14  22487  isfil  22716  isufil  22772  isufl  22782  flfcntr  22912  ucnval  23146  iscusp  23168  prdsxmslem2  23399  tngngp3  23526  isnlm  23545  nmofval  23584  lebnumii  23835  iscau4  24148  iscmet  24153  iscmet3lem1  24160  iscmet3  24162  equivcmet  24186  ulmcaulem  25258  ulmcau  25259  fsumdvdscom  26039  dchrisumlem3  26344  pntibndlem2  26444  pntibnd  26446  pntlemp  26463  ostth2lem2  26487  trgcgrg  26578  tgcgr4  26594  isismt  26597  nbgr2vtx1edg  27410  nbuhgr2vtx1edgb  27412  uvtxval  27447  uvtxel  27448  uvtxel1  27456  uvtxusgrel  27463  cusgredg  27484  cplgr3v  27495  cplgrop  27497  usgredgsscusgredg  27519  isrgr  27619  isewlk  27662  iswlk  27670  iswwlks  27892  wlkiswwlks2  27931  isclwwlk  28039  clwlkclwwlklem1  28054  isconngr  28244  isconngr1  28245  isfrgr  28315  frgr1v  28326  nfrgr2v  28327  frgr3v  28330  1vwmgr  28331  3vfriswmgr  28333  3cyclfrgrrn1  28340  n4cyclfrgr  28346  isplig  28529  gidval  28565  vciOLD  28614  isvclem  28630  isnvlem  28663  lnoval  28805  ajfval  28862  isphg  28870  minvecolem3  28929  htth  28971  ressprs  30932  mntoval  30951  mgcoval  30955  isslmd  31146  resv1r  31227  prmidlval  31298  mxidlval  31319  isufd  31349  rprmval  31350  iscref  31480  ordtrest2NEW  31559  fmcncfil  31567  issiga  31764  isrnsiga  31765  isldsys  31808  ismeas  31851  carsgval  31954  issibf  31984  sitgfval  31992  signstfvneq0  32235  istrkg2d  32330  ispconn  32870  issconn  32873  txpconn  32879  cvxpconn  32889  cvmscbv  32905  iscvm  32906  cvmsdisj  32917  cvmsss2  32921  snmlval  32978  elmrsubrn  33167  ismfs  33196  mclsval  33210  on2ind  33522  on3ind  33523  madebdayim  33764  no2indslem  33805  no3inds  33809  fwddifnval  34159  bj-ismoore  34968  pibp19  35279  pibp21  35280  poimirlem28  35499  cover2g  35567  seqpo  35599  incsequz2  35601  caushft  35613  ismtyval  35652  isass  35698  isexid  35699  elghomlem1OLD  35737  isrngo  35749  isrngod  35750  isgrpda  35807  rngohomval  35816  iscom2  35847  idlval  35865  pridlval  35885  maxidlval  35891  elrefrels3  36330  elcnvrefrels3  36343  eleqvrels3  36400  lflset  36767  islfld  36770  isopos  36888  isoml  36946  isatl  37007  iscvlat  37031  ishlat1  37060  psubspset  37452  lautset  37790  pautsetN  37806  ldilfset  37816  ltrnfset  37825  dilfsetN  37860  trnfsetN  37863  trnsetN  37864  trlfset  37868  tendofset  38466  tendoset  38467  dihffval  38938  lpolsetN  39190  hdmapfval  39535  hgmapfval  39594  aomclem8  40541  islnm  40557  clsk1independent  41285  gneispace2  41371  gneispaceel2  41383  gneispacess2  41385  ioodvbdlimc1lem1  43101  ioodvbdlimc1lem2  43102  ioodvbdlimc2lem  43104  issal  43484  ismea  43618  isome  43661  iccpartiltu  44501  iccelpart  44512  isomgr  44902  isupwlk  44925  mgmpropd  44956  ismgmd  44957  ismgmhm  44964  resmgmhm  44979  iscllaw  45010  iscomlaw  45011  isasslaw  45013  isrng  45061  c0snmgmhm  45099  zlidlring  45113  uzlidlring  45114  dmatALTval  45368  islininds  45414  lindslinindsimp2  45431  ldepsnlinc  45476  elbigo  45524  iscnrm3r  45869  isprsd  45876  lubeldm2d  45879  glbeldm2d  45880  isthincd2lem2  45944  isthincd  45945