Theorem raleqbidv 3344

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  rspc2vd  3907  frd  5619  f12dfv  7272  f13dfv  7273  knatar  7356  ofrfvalg  7683  fmpox  8064  ovmptss  8088  frrlem4  8286  on2ind  8655  on3ind  8656  marypha1lem  9393  supeq123d  9410  oieq1  9474  acneq  10027  isfin1a  10276  fpwwe2cbv  10615  fpwwe2lem2  10617  fpwwecbv  10629  fpwwelem  10630  eltskg  10735  elgrug  10777  cau3lem  15406  rlim  15546  ello1  15566  elo1  15577  caurcvg2  15729  caucvgb  15731  fsum2dlem  15821  fsumcom2  15825  fprod2dlem  16034  fprodcom2  16038  pcfac  16959  vdwpc  17040  rami  17075  prmgaplem7  17117  prdsval  17508  ismre  17642  isacs2  17709  acsfiel  17710  iscat  17728  iscatd  17729  catidex  17730  catideu  17731  cidfval  17732  cidval  17733  catlid  17739  catrid  17740  comfeq  17762  catpropd  17765  monfval  17789  issubc  17892  fullsubc  17907  isfunc  17921  funcpropd  17959  isfull  17969  isfth  17973  fthpropd  17980  natfval  18006  initoval  18050  termoval  18051  isposd  18378  lubfval  18404  glbfval  18417  ischn  18663  chnind  18677  chnub  18678  ismgm  18699  mgmpropd  18709  ismgmd  18710  issstrmgm  18711  grpidval  18719  gsumvalx  18734  gsumpropd  18736  gsumress  18740  ismgmhm  18754  resmgmhm  18769  issgrp  18778  sgrppropd  18789  ismnddef  18794  ismndd  18814  mndpropd  18817  ismhm  18843  resmhm  18879  isgrp  19006  grppropd  19018  isgrpd2e  19022  isnsg  19221  nmznsg  19234  isghm  19286  isga  19361  subgga  19370  gsmsymgrfix  19498  gsmsymgreq  19502  gexval  19648  ispgp  19662  isslw  19678  sylow2blem2  19691  efgval  19787  efgi  19789  efgsdm  19800  cmnpropd  19861  iscmnd  19864  submcmn2  19909  gsumzaddlem  19991  dmdprd  20070  dprdcntz  20080  isrng  20232  rngpropd  20252  issrg  20270  isring  20319  ringpropd  20371  isirred  20501  c0snmgmhm  20544  islring  20625  rrgval  20782  isdomn  20790  sdrgacs  20882  abvfval  20891  abvpropd  20916  islmod  20963  islmodd  20965  lmodprop2d  21023  lssset  21032  islmhm  21126  reslmhm  21151  lmhmpropd  21172  islbs  21175  prmidlval  21433  psgndiflemA  21720  isphl  21747  islindf  21931  islindf2  21933  lsslindf  21949  isassa  21975  isassad  21984  assapropd  21990  ltbval  22163  opsrval  22166  dmatval  22618  dmatcrng  22628  scmatcrng  22647  cpmat  22835  istopg  23021  restbas  23284  ordtrest2  23330  cnfval  23359  cnpfval  23360  ist0  23446  ist1  23447  ishaus  23448  iscnrm  23449  isnrm  23461  ist0-2  23470  ishaus2  23477  nrmsep3  23481  iscmp  23514  is1stc  23567  isptfin  23642  islocfin  23643  kgenval  23661  kgencn2  23683  txbas  23693  ptval  23696  dfac14  23744  isfil  23973  isufil  24029  isufl  24039  flfcntr  24169  ucnval  24402  iscusp  24424  prdsxmslem2  24655  tngngp3  24782  isnlm  24801  nmofval  24840  lebnumii  25094  iscau4  25407  iscmet  25412  iscmet3lem1  25419  iscmet3  25421  equivcmet  25445  ulmcaulem  26523  ulmcau  26524  fsumdvdscom  27315  dchrisumlem3  27621  pntibndlem2  27721  pntibnd  27723  pntlemp  27740  ostth2lem2  27764  madebdayim  28047  no2indlesm  28113  no3inds  28117  istrkgc  28689  istrkgb  28690  istrkge  28692  trgcgrg  28750  tgcgr4  28766  isismt  28769  nbgr2vtx1edg  29641  nbuhgr2vtx1edgb  29643  uvtxval  29678  uvtxel  29679  uvtxel1  29687  uvtxusgrel  29694  cusgredg  29715  cplgr3v  29726  cplgrop  29728  usgredgsscusgredg  29750  isrgr  29850  isewlk  29893  iswlk  29901  iswwlks  30126  wlkiswwlks2  30165  isclwwlk  30276  clwlkclwwlklem1  30291  isconngr  30481  isconngr1  30482  isfrgr  30552  frgr1v  30563  nfrgr2v  30564  frgr3v  30567  1vwmgr  30568  3vfriswmgr  30570  3cyclfrgrrn1  30577  n4cyclfrgr  30583  isplig  30769  gidval  30805  vciOLD  30854  isvclem  30870  isnvlem  30903  lnoval  31045  ajfval  31102  isphg  31110  minvecolem3  31169  htth  31211  ressprs  33227  mntoval  33243  mgcoval  33247  fxpval  33426  isslmd  33463  resv1r  33602  mxidlval  33689  rprmval  33751  isufd  33775  vieta  33915  constrconj  34080  iscref  34179  ordtrest2NEW  34258  fmcncfil  34266  issiga  34447  isrnsiga  34448  isldsys  34491  ismeas  34534  carsgval  34638  issibf  34668  sitgfval  34676  signstfvneq0  34904  istrkg2d  34998  ispconn  35648  issconn  35651  txpconn  35657  cvxpconn  35667  cvmscbv  35683  iscvm  35684  cvmsdisj  35695  cvmsss2  35699  snmlval  35756  elmrsubrn  35945  ismfs  35974  mclsval  35988  fwddifnval  36588  weiunfrlem  36898  bj-ismoore  37670  pibp19  37983  pibp21  37984  poimirlem28  38222  cover2g  38290  seqpo  38321  incsequz2  38323  caushft  38335  ismtyval  38374  isass  38420  isexid  38421  elghomlem1OLD  38459  isrngo  38471  isrngod  38472  isgrpda  38529  rngohomval  38538  iscom2  38569  idlval  38587  pridlval  38607  maxidlval  38613  elrefrels3  39173  elcnvrefrels3  39189  eleqvrels3  39251  lflset  39758  islfld  39761  isopos  39879  isoml  39937  isatl  39998  iscvlat  40022  ishlat1  40051  psubspset  40443  lautset  40781  pautsetN  40797  ldilfset  40807  ltrnfset  40816  dilfsetN  40851  trnfsetN  40854  trnsetN  40855  trlfset  40859  tendofset  41457  tendoset  41458  dihffval  41929  lpolsetN  42181  hdmapfval  42526  hgmapfval  42585  sn-isghm  43332  aomclem8  43715  islnm  43731  clsk1independent  44699  gneispace2  44785  gneispaceel2  44797  gneispacess2  44799  caucvgbf  46130  ioodvbdlimc1lem1  46572  ioodvbdlimc1lem2  46573  ioodvbdlimc2lem  46575  issal  46955  ismea  47092  isome  47135  chnerlem1  47525  iccpartiltu  48095  iccelpart  48106  isgrim  48571  isubgrgrim  48618  isgrlim  48671  usgrexmpl2trifr  48726  gpg5nbgr3star  48770  isupwlk  48825  iscllaw  48878  iscomlaw  48879  isasslaw  48881  zlidlring  48923  uzlidlring  48924  dmatALTval  49100  islininds  49146  lindslinindsimp2  49163  ldepsnlinc  49208  elbigo  49251  iscnrm3r  49646  isprsd  49653  lubeldm2d  49656  glbeldm2d  49657  nelsubc3lem  49768  ssccatid  49770  resccatlem  49771  upciclem1  49864  upfval  49874  upfval2  49875  upfval3  49876  oppcup3lem  49904  oppcup  49905  uptr2  49919  isthincd2lem2  50133  isthincd  50134  thincpropd  50140