Theorem raleqbidv 3319

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspc2vd  3910  frd  5595  f12dfv  7248  f13dfv  7249  knatar  7332  ofrfvalg  7661  fmpox  8046  ovmptss  8072  frrlem4  8268  on2ind  8633  on3ind  8634  marypha1lem  9384  supeq123d  9401  oieq1  9465  acneq  9996  isfin1a  10245  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwecbv  10597  fpwwelem  10598  eltskg  10703  elgrug  10745  cau3lem  15321  rlim  15461  ello1  15481  elo1  15492  caurcvg2  15644  caucvgb  15646  fsum2dlem  15736  fsumcom2  15740  fprod2dlem  15946  fprodcom2  15950  pcfac  16870  vdwpc  16951  rami  16986  prmgaplem7  17028  prdsval  17418  ismre  17551  isacs2  17614  acsfiel  17615  iscat  17633  iscatd  17634  catidex  17635  catideu  17636  cidfval  17637  cidval  17638  catlid  17644  catrid  17645  comfeq  17667  catpropd  17670  monfval  17694  issubc  17797  fullsubc  17812  isfunc  17826  funcpropd  17864  isfull  17874  isfth  17878  fthpropd  17885  natfval  17911  initoval  17955  termoval  17956  isposd  18283  lubfval  18309  glbfval  18322  ismgm  18568  mgmpropd  18578  ismgmd  18579  issstrmgm  18580  grpidval  18588  gsumvalx  18603  gsumpropd  18605  gsumress  18609  ismgmhm  18623  resmgmhm  18638  issgrp  18647  sgrppropd  18658  ismnddef  18663  ismndd  18683  mndpropd  18686  ismhm  18712  resmhm  18747  isgrp  18871  grppropd  18883  isgrpd2e  18887  isnsg  19087  nmznsg  19100  isghm  19147  isghmOLD  19148  isga  19223  subgga  19232  gsmsymgrfix  19358  gsmsymgreq  19362  gexval  19508  ispgp  19522  isslw  19538  sylow2blem2  19551  efgval  19647  efgi  19649  efgsdm  19660  cmnpropd  19721  iscmnd  19724  submcmn2  19769  gsumzaddlem  19851  dmdprd  19930  dprdcntz  19940  isrng  20063  rngpropd  20083  issrg  20097  isring  20146  ringpropd  20197  isirred  20328  c0snmgmhm  20371  islring  20449  rrgval  20606  isdomn  20614  sdrgacs  20710  abvfval  20719  abvpropd  20744  islmod  20770  islmodd  20772  lmodprop2d  20830  lssset  20839  islmhm  20934  reslmhm  20959  lmhmpropd  20980  islbs  20983  psgndiflemA  21510  isphl  21537  islindf  21721  islindf2  21723  lsslindf  21739  isassa  21765  isassad  21774  assapropd  21781  ltbval  21950  opsrval  21953  dmatval  22379  dmatcrng  22389  scmatcrng  22408  cpmat  22596  istopg  22782  restbas  23045  ordtrest2  23091  cnfval  23120  cnpfval  23121  ist0  23207  ist1  23208  ishaus  23209  iscnrm  23210  isnrm  23222  ist0-2  23231  ishaus2  23238  nrmsep3  23242  iscmp  23275  is1stc  23328  isptfin  23403  islocfin  23404  kgenval  23422  kgencn2  23444  txbas  23454  ptval  23457  dfac14  23505  isfil  23734  isufil  23790  isufl  23800  flfcntr  23930  ucnval  24164  iscusp  24186  prdsxmslem2  24417  tngngp3  24544  isnlm  24563  nmofval  24602  lebnumii  24865  iscau4  25179  iscmet  25184  iscmet3lem1  25191  iscmet3  25193  equivcmet  25217  ulmcaulem  26303  ulmcau  26304  fsumdvdscom  27095  dchrisumlem3  27402  pntibndlem2  27502  pntibnd  27504  pntlemp  27521  ostth2lem2  27545  madebdayim  27799  no2indslem  27861  no3inds  27865  istrkgc  28381  istrkgb  28382  istrkge  28384  trgcgrg  28442  tgcgr4  28458  isismt  28461  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  uvtxval  29314  uvtxel  29315  uvtxel1  29323  uvtxusgrel  29330  cusgredg  29351  cplgr3v  29362  cplgrop  29364  usgredgsscusgredg  29387  isrgr  29487  isewlk  29530  iswlk  29538  iswwlks  29766  wlkiswwlks2  29805  isclwwlk  29913  clwlkclwwlklem1  29928  isconngr  30118  isconngr1  30119  isfrgr  30189  frgr1v  30200  nfrgr2v  30201  frgr3v  30204  1vwmgr  30205  3vfriswmgr  30207  3cyclfrgrrn1  30214  n4cyclfrgr  30220  isplig  30405  gidval  30441  vciOLD  30490  isvclem  30506  isnvlem  30539  lnoval  30681  ajfval  30738  isphg  30746  minvecolem3  30805  htth  30847  ressprs  32890  mntoval  32908  mgcoval  32912  ischn  32932  chnind  32937  chnub  32938  fxpval  33122  isslmd  33155  resv1r  33311  prmidlval  33408  mxidlval  33432  rprmval  33487  isufd  33511  constrconj  33735  iscref  33834  ordtrest2NEW  33913  fmcncfil  33921  issiga  34102  isrnsiga  34103  isldsys  34146  ismeas  34189  carsgval  34294  issibf  34324  sitgfval  34332  signstfvneq0  34563  istrkg2d  34657  ispconn  35210  issconn  35213  txpconn  35219  cvxpconn  35229  cvmscbv  35245  iscvm  35246  cvmsdisj  35257  cvmsss2  35261  snmlval  35318  elmrsubrn  35507  ismfs  35536  mclsval  35550  fwddifnval  36151  weiunfrlem  36452  bj-ismoore  37093  pibp19  37402  pibp21  37403  poimirlem28  37642  cover2g  37710  seqpo  37741  incsequz2  37743  caushft  37755  ismtyval  37794  isass  37840  isexid  37841  elghomlem1OLD  37879  isrngo  37891  isrngod  37892  isgrpda  37949  rngohomval  37958  iscom2  37989  idlval  38007  pridlval  38027  maxidlval  38033  elrefrels3  38510  elcnvrefrels3  38526  eleqvrels3  38584  lflset  39052  islfld  39055  isopos  39173  isoml  39231  isatl  39292  iscvlat  39316  ishlat1  39345  psubspset  39738  lautset  40076  pautsetN  40092  ldilfset  40102  ltrnfset  40111  dilfsetN  40146  trnfsetN  40149  trnsetN  40150  trlfset  40154  tendofset  40752  tendoset  40753  dihffval  41224  lpolsetN  41476  hdmapfval  41821  hgmapfval  41880  sn-isghm  42661  aomclem8  43050  islnm  43066  clsk1independent  44035  gneispace2  44121  gneispaceel2  44133  gneispacess2  44135  caucvgbf  45485  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  issal  46312  ismea  46449  isome  46492  iccpartiltu  47423  iccelpart  47434  isgrim  47882  isubgrgrim  47929  isgrlim  47981  usgrexmpl2trifr  48028  gpg5nbgr3star  48072  isupwlk  48124  iscllaw  48177  iscomlaw  48178  isasslaw  48180  zlidlring  48222  uzlidlring  48223  dmatALTval  48389  islininds  48435  lindslinindsimp2  48452  ldepsnlinc  48497  elbigo  48540  iscnrm3r  48936  isprsd  48943  lubeldm2d  48946  glbeldm2d  48947  nelsubc3lem  49059  ssccatid  49061  resccatlem  49062  upciclem1  49155  upfval  49165  upfval2  49166  upfval3  49167  oppcup3lem  49195  oppcup  49196  uptr2  49210  isthincd2lem2  49424  isthincd  49425  thincpropd  49431