Theorem raleqbidv 3336

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-ral 3079

This theorem is used by:  rspc2vd  3898  frd  5616  f12dfv  7277  f13dfv  7278  knatar  7363  ofrfvalg  7689  fmpox  8067  ovmptss  8093  frrlem4  8291  on2ind  8660  on3ind  8661  marypha1lem  9406  supeq123d  9423  oieq1  9487  acneq  10049  isfin1a  10297  fpwwe2cbv  10642  fpwwe2lem2  10644  fpwwecbv  10656  fpwwelem  10657  eltskg  10762  elgrug  10804  cau3lem  15444  rlim  15584  ello1  15604  elo1  15615  caurcvg2  15767  caucvgb  15769  fsum2dlem  15858  fsumcom2  15862  fprod2dlem  16071  fprodcom2  16075  pcfac  16995  vdwpc  17076  rami  17111  prmgaplem7  17153  prdsval  17544  ismre  17678  isacs2  17745  acsfiel  17746  iscat  17764  iscatd  17765  catidex  17766  catideu  17767  cidfval  17768  cidval  17769  catlid  17775  catrid  17776  comfeq  17798  catpropd  17801  monfval  17825  issubc  17928  fullsubc  17943  isfunc  17957  funcpropd  17995  isfull  18005  isfth  18009  fthpropd  18016  natfval  18042  initoval  18086  termoval  18087  isposd  18414  lubfval  18440  glbfval  18453  ischn  18699  chnind  18713  chnub  18714  ismgm  18735  mgmpropd  18747  ismgmd  18748  issstrmgm  18749  grpidval  18758  idressid  18779  gsumvalx  18780  gsumpropd  18782  gsumress  18786  ismgmhm  18800  resmgmhm  18815  issgrp  18824  sgrppropd  18835  ismnddef  18840  ismndd  18861  mndpropd  18866  ismhm  18894  resmhm  18930  isgrp  19064  grppropd  19076  isgrpd2e  19080  isnsg  19279  nmznsg  19292  isghm  19344  isga  19419  subgga  19428  gsmsymgrfix  19556  gsmsymgreq  19560  gexval  19706  ispgp  19720  isslw  19736  sylow2blem2  19749  efgval  19845  efgi  19847  efgsdm  19858  cmnpropd  19919  iscmnd  19922  submcmn2  19967  gsumzaddlem  20049  dmdprd  20128  dprdcntz  20138  isrng  20290  rngpropd  20310  issrg  20328  isring  20377  ringpropd  20431  isirred  20561  c0snmgmhm  20604  islring  20703  rrgval  20860  isdomn  20868  sdrgacs  20968  abvfval  20977  abvpropd  21002  islmod  21049  islmodd  21051  lmodprop2d  21109  lssset  21118  islmhm  21212  reslmhm  21237  lmhmpropd  21258  islbs  21261  prmidlval  21526  psgndiflemA  21815  isphl  21842  islindf  22026  islindf2  22028  lsslindf  22044  isassa  22072  isassad  22081  assapropd  22087  ltbval  22260  opsrval  22263  dmatval  22715  dmatcrng  22725  scmatcrng  22744  cpmat  22935  istopg  23121  restbas  23384  ordtrest2  23430  cnfval  23459  cnpfval  23460  ist0  23546  ist1  23547  ishaus  23548  iscnrm  23549  isnrm  23561  ist0-2  23570  ishaus2  23577  nrmsep3  23581  iscmp  23614  is1stc  23667  isptfin  23743  islocfin  23744  kgenval  23762  kgencn2  23784  txbas  23794  ptval  23797  dfac14  23845  isfil  24074  isufil  24130  isufl  24140  flfcntr  24270  ucnval  24503  iscusp  24525  prdsxmslem2  24756  tngngp3  24883  isnlm  24902  nmofval  24941  lebnumii  25195  iscau4  25508  iscmet  25513  iscmet3lem1  25520  iscmet3  25522  equivcmet  25546  ulmcaulem  26627  ulmcau  26628  fsumdvdscom  27419  dchrisumlem3  27725  pntibndlem2  27825  pntibnd  27827  pntlemp  27844  ostth2lem2  27868  madebdayim  28151  no2indlesm  28217  no3inds  28221  istrkgc  28793  istrkgb  28794  istrkge  28796  trgcgrg  28855  tgcgr4  28871  isismt  28874  nbgr2vtx1edg  29796  nbuhgr2vtx1edgb  29798  uvtxval  29833  uvtxel  29834  uvtxel1  29842  uvtxusgrel  29849  cusgredg  29870  cplgr3v  29881  cplgrop  29883  usgredgsscusgredg  29905  isrgr  30005  isewlk  30048  iswlk  30056  iswwlks  30290  wlkiswwlks2  30329  isclwwlk  30440  clwlkclwwlklem1  30455  isconngr  30655  isconngr1  30656  isfrgr  30726  frgr1v  30737  nfrgr2v  30738  frgr3v  30741  1vwmgr  30742  3vfriswmgr  30744  3cyclfrgrrn1  30751  n4cyclfrgr  30757  isplig  30943  gidval  30979  vciOLD  31028  isvclem  31044  isnvlem  31077  lnoval  31219  ajfval  31276  isphg  31284  minvecolem3  31343  htth  31385  ressprs  33393  mntoval  33409  mgcoval  33413  fxpval  33592  isslmd  33629  resv1r  33766  mxidlval  33851  rprmval  33913  isufd  33937  vieta  34077  constrconj  34242  iscref  34341  ordtrest2NEW  34420  fmcncfil  34428  issiga  34609  isrnsiga  34610  isldsys  34654  ismeas  34697  carsgval  34801  issibf  34831  sitgfval  34839  signstfvneq0  35067  istrkg2d  35161  ispconn  35789  issconn  35792  txpconn  35798  cvxpconn  35808  cvmscbv  35824  iscvm  35825  cvmsdisj  35836  cvmsss2  35840  snmlval  35897  elmrsubrn  36086  ismfs  36115  mclsval  36129  fwddifnval  36730  weiunfrlem  37070  bj-ismoore  37842  pibp19  38155  pibp21  38156  poimirlem28  38384  cover2g  38453  seqpo  38484  incsequz2  38486  caushft  38498  ismtyval  38537  isass  38583  isexid  38584  elghomlem1OLD  38622  isrngo  38634  isrngod  38635  isgrpda  38692  rngohomval  38701  iscom2  38732  idlval  38750  pridlval  38770  maxidlval  38776  elrefrels3  39334  elcnvrefrels3  39350  eleqvrels3  39412  lflset  39919  islfld  39922  isopos  40040  isoml  40098  isatl  40159  iscvlat  40183  ishlat1  40212  psubspset  40604  lautset  40942  pautsetN  40958  ldilfset  40968  ltrnfset  40977  dilfsetN  41012  trnfsetN  41015  trnsetN  41016  trlfset  41020  tendofset  41618  tendoset  41619  dihffval  42090  lpolsetN  42342  hdmapfval  42687  hgmapfval  42746  sn-isghm  43506  aomclem8  43889  islnm  43905  clsk1independent  44873  gneispace2  44959  gneispaceel2  44971  gneispacess2  44973  caucvgbf  46304  ioodvbdlimc1lem1  46746  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  issal  47129  ismea  47266  isome  47309  chnerlem1  47697  tmachlem-agreesn  47762  iccpartiltu  48309  iccelpart  48320  isgrim  48785  isubgrgrim  48832  isgrlim  48885  usgrexmpl2trifr  48940  gpg5nbgr3star  48984  isupwlk  49039  iscllaw  49091  iscomlaw  49092  isasslaw  49094  zlidlring  49136  uzlidlring  49137  dmatALTval  49317  islininds  49363  lindslinindsimp2  49380  ldepsnlinc  49425  elbigo  49468  iscnrm3r  49861  isprsd  49868  lubeldm2d  49871  glbeldm2d  49872  nelsubc3lem  49983  ssccatid  49985  resccatlem  49986  upciclem1  50079  upfval  50089  upfval2  50090  upfval3  50091  oppcup3lem  50119  oppcup  50120  uptr2  50134  isthincd2lem2  50348  isthincd  50349  thincpropd  50355