Theorem raleqbidv 3325

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-ral 3052

This theorem is referenced by:  rspc2vd  3922  frd  5610  f12dfv  7265  f13dfv  7266  knatar  7349  ofrfvalg  7677  fmpox  8064  ovmptss  8090  frrlem4  8286  on2ind  8679  on3ind  8680  marypha1lem  9443  supeq123d  9460  oieq1  9524  acneq  10055  isfin1a  10304  fpwwe2cbv  10642  fpwwe2lem2  10644  fpwwecbv  10656  fpwwelem  10657  eltskg  10762  elgrug  10804  cau3lem  15371  rlim  15509  ello1  15529  elo1  15540  caurcvg2  15692  caucvgb  15694  fsum2dlem  15784  fsumcom2  15788  fprod2dlem  15994  fprodcom2  15998  pcfac  16917  vdwpc  16998  rami  17033  prmgaplem7  17075  prdsval  17467  ismre  17600  isacs2  17663  acsfiel  17664  iscat  17682  iscatd  17683  catidex  17684  catideu  17685  cidfval  17686  cidval  17687  catlid  17693  catrid  17694  comfeq  17716  catpropd  17719  monfval  17743  issubc  17846  fullsubc  17861  isfunc  17875  funcpropd  17913  isfull  17923  isfth  17927  fthpropd  17934  natfval  17960  initoval  18004  termoval  18005  isposd  18332  lubfval  18358  glbfval  18371  ismgm  18617  mgmpropd  18627  ismgmd  18628  issstrmgm  18629  grpidval  18637  gsumvalx  18652  gsumpropd  18654  gsumress  18658  ismgmhm  18672  resmgmhm  18687  issgrp  18696  sgrppropd  18707  ismnddef  18712  ismndd  18732  mndpropd  18735  ismhm  18761  resmhm  18796  isgrp  18920  grppropd  18932  isgrpd2e  18936  isnsg  19136  nmznsg  19149  isghm  19196  isghmOLD  19197  isga  19272  subgga  19281  gsmsymgrfix  19407  gsmsymgreq  19411  gexval  19557  ispgp  19571  isslw  19587  sylow2blem2  19600  efgval  19696  efgi  19698  efgsdm  19709  cmnpropd  19770  iscmnd  19773  submcmn2  19818  gsumzaddlem  19900  dmdprd  19979  dprdcntz  19989  isrng  20112  rngpropd  20132  issrg  20146  isring  20195  ringpropd  20246  isirred  20377  c0snmgmhm  20420  islring  20498  rrgval  20655  isdomn  20663  sdrgacs  20759  abvfval  20768  abvpropd  20793  islmod  20819  islmodd  20821  lmodprop2d  20879  lssset  20888  islmhm  20983  reslmhm  21008  lmhmpropd  21029  islbs  21032  psgndiflemA  21559  isphl  21586  islindf  21770  islindf2  21772  lsslindf  21788  isassa  21814  isassad  21823  assapropd  21830  ltbval  21999  opsrval  22002  dmatval  22428  dmatcrng  22438  scmatcrng  22457  cpmat  22645  istopg  22831  restbas  23094  ordtrest2  23140  cnfval  23169  cnpfval  23170  ist0  23256  ist1  23257  ishaus  23258  iscnrm  23259  isnrm  23271  ist0-2  23280  ishaus2  23287  nrmsep3  23291  iscmp  23324  is1stc  23377  isptfin  23452  islocfin  23453  kgenval  23471  kgencn2  23493  txbas  23503  ptval  23506  dfac14  23554  isfil  23783  isufil  23839  isufl  23849  flfcntr  23979  ucnval  24213  iscusp  24235  prdsxmslem2  24466  tngngp3  24593  isnlm  24612  nmofval  24651  lebnumii  24914  iscau4  25229  iscmet  25234  iscmet3lem1  25241  iscmet3  25243  equivcmet  25267  ulmcaulem  26353  ulmcau  26354  fsumdvdscom  27145  dchrisumlem3  27452  pntibndlem2  27552  pntibnd  27554  pntlemp  27571  ostth2lem2  27595  madebdayim  27843  no2indslem  27904  no3inds  27908  istrkgc  28379  istrkgb  28380  istrkge  28382  trgcgrg  28440  tgcgr4  28456  isismt  28459  nbgr2vtx1edg  29275  nbuhgr2vtx1edgb  29277  uvtxval  29312  uvtxel  29313  uvtxel1  29321  uvtxusgrel  29328  cusgredg  29349  cplgr3v  29360  cplgrop  29362  usgredgsscusgredg  29385  isrgr  29485  isewlk  29528  iswlk  29536  iswwlks  29764  wlkiswwlks2  29803  isclwwlk  29911  clwlkclwwlklem1  29926  isconngr  30116  isconngr1  30117  isfrgr  30187  frgr1v  30198  nfrgr2v  30199  frgr3v  30202  1vwmgr  30203  3vfriswmgr  30205  3cyclfrgrrn1  30212  n4cyclfrgr  30218  isplig  30403  gidval  30439  vciOLD  30488  isvclem  30504  isnvlem  30537  lnoval  30679  ajfval  30736  isphg  30744  minvecolem3  30803  htth  30845  ressprs  32890  mntoval  32908  mgcoval  32912  ischn  32932  chnind  32937  chnub  32938  isslmd  33145  resv1r  33301  prmidlval  33398  mxidlval  33422  rprmval  33477  isufd  33501  constrconj  33725  iscref  33821  ordtrest2NEW  33900  fmcncfil  33908  issiga  34089  isrnsiga  34090  isldsys  34133  ismeas  34176  carsgval  34281  issibf  34311  sitgfval  34319  signstfvneq0  34550  istrkg2d  34644  ispconn  35191  issconn  35194  txpconn  35200  cvxpconn  35210  cvmscbv  35226  iscvm  35227  cvmsdisj  35238  cvmsss2  35242  snmlval  35299  elmrsubrn  35488  ismfs  35517  mclsval  35531  fwddifnval  36127  weiunfrlem  36428  bj-ismoore  37069  pibp19  37378  pibp21  37379  poimirlem28  37618  cover2g  37686  seqpo  37717  incsequz2  37719  caushft  37731  ismtyval  37770  isass  37816  isexid  37817  elghomlem1OLD  37855  isrngo  37867  isrngod  37868  isgrpda  37925  rngohomval  37934  iscom2  37965  idlval  37983  pridlval  38003  maxidlval  38009  elrefrels3  38483  elcnvrefrels3  38499  eleqvrels3  38557  lflset  39023  islfld  39026  isopos  39144  isoml  39202  isatl  39263  iscvlat  39287  ishlat1  39316  psubspset  39709  lautset  40047  pautsetN  40063  ldilfset  40073  ltrnfset  40082  dilfsetN  40117  trnfsetN  40120  trnsetN  40121  trlfset  40125  tendofset  40723  tendoset  40724  dihffval  41195  lpolsetN  41447  hdmapfval  41792  hgmapfval  41851  sn-isghm  42643  aomclem8  43032  islnm  43048  clsk1independent  44017  gneispace2  44103  gneispaceel2  44115  gneispacess2  44117  caucvgbf  45464  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  issal  46291  ismea  46428  isome  46471  iccpartiltu  47384  iccelpart  47395  isgrim  47843  isubgrgrim  47890  isgrlim  47942  usgrexmpl2trifr  47989  gpg5nbgr3star  48031  isupwlk  48059  iscllaw  48112  iscomlaw  48113  isasslaw  48115  zlidlring  48157  uzlidlring  48158  dmatALTval  48324  islininds  48370  lindslinindsimp2  48387  ldepsnlinc  48432  elbigo  48479  iscnrm3r  48870  isprsd  48877  lubeldm2d  48880  glbeldm2d  48881  nelsubc3lem  48985  ssccatid  48987  resccatlem  48988  upciclem1  49049  upfval  49059  upfval2  49060  upfval3  49061  oppcup3lem  49087  oppcup  49088  isthincd2lem2  49269  isthincd  49270  thincpropd  49276