Theorem raleqbidv 3334

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 2213 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 2846	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	imbi12d 347	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))
5	4	ralbidv2 3181	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rspc2vd  3895  frd  5605  f12dfv  7270  f13dfv  7271  knatar  7356  ofrfvalg  7685  fmpox  8062  ovmptss  8088  frrlem4  8286  on2ind  8657  on3ind  8658  marypha1lem  9403  supeq123d  9420  oieq1  9484  acneq  10079  isfin1a  10327  fpwwe2cbv  10672  fpwwe2lem2  10674  fpwwecbv  10686  fpwwelem  10687  eltskg  10792  elgrug  10834  cau3lem  15475  rlim  15615  ello1  15635  elo1  15646  caurcvg2  15798  caucvgb  15800  fsum2dlem  15889  fsumcom2  15893  fprod2dlem  16100  fprodcom2  16104  pcfac  17024  vdwpc  17105  rami  17140  prmgaplem7  17182  prdsval  17573  ismre  17707  isacs2  17774  acsfiel  17775  iscat  17793  iscatd  17794  catidex  17795  catideu  17796  cidfval  17797  cidval  17798  catlid  17804  catrid  17805  comfeq  17827  catpropd  17830  monfval  17854  issubc  17957  fullsubc  17972  isfunc  17986  funcpropd  18024  isfull  18034  isfth  18038  fthpropd  18045  natfval  18071  initoval  18115  termoval  18116  isposd  18443  lubfval  18469  glbfval  18482  ischn  18728  chnind  18742  chnub  18743  ismgm  18764  mgmpropd  18776  ismgmd  18777  issstrmgm  18778  grpidval  18787  idressid  18809  gsumvalx  18812  gsumpropd  18814  gsumress  18818  ismgmhm  18832  resmgmhm  18847  issgrp  18856  sgrppropd  18867  ismnddef  18872  ismndd  18893  mndpropd  18898  ismhm  18927  resmhm  18963  isgrp  19097  grppropd  19109  isgrpd2e  19113  isnsg  19312  nmznsg  19325  isghm  19377  isga  19452  subgga  19461  gsmsymgrfix  19589  gsmsymgreq  19593  gexval  19739  ispgp  19753  isslw  19769  sylow2blem2  19782  efgval  19878  efgi  19880  efgsdm  19891  cmnpropd  19952  iscmnd  19955  submcmn2  20000  gsumzaddlem  20082  dmdprd  20161  dprdcntz  20171  isrng  20323  rngpropd  20343  issrg  20361  isring  20410  ringpropd  20466  isirred  20596  c0snmgmhm  20639  islring  20739  rrgval  20896  isdomn  20904  sdrgacs  21005  abvfval  21014  abvpropd  21039  islmod  21086  islmodd  21088  lmodprop2d  21146  lssset  21155  islmhm  21249  reslmhm  21274  lmhmpropd  21295  islbs  21298  prmidlval  21565  psgndiflemA  21854  isphl  21881  islindf  22065  islindf2  22067  lsslindf  22083  isassa  22111  isassad  22120  assapropd  22126  ltbval  22299  opsrval  22302  dmatval  22754  dmatcrng  22764  scmatcrng  22783  cpmat  22974  istopg  23160  restbas  23423  ordtrest2  23469  cnfval  23498  cnpfval  23499  ist0  23585  ist1  23586  ishaus  23587  iscnrm  23588  isnrm  23600  ist0-2  23609  ishaus2  23616  nrmsep3  23620  iscmp  23653  is1stc  23706  isptfin  23782  islocfin  23783  kgenval  23801  kgencn2  23823  txbas  23833  ptval  23836  dfac14  23884  isfil  24113  isufil  24169  isufl  24179  flfcntr  24309  ucnval  24542  iscusp  24564  prdsxmslem2  24795  tngngp3  24922  isnlm  24941  nmofval  24980  lebnumii  25234  iscau4  25547  iscmet  25552  iscmet3lem1  25559  iscmet3  25561  equivcmet  25585  ulmcaulem  26670  ulmcau  26671  fsumdvdscom  27461  dchrisumlem3  27767  pntibndlem2  27867  pntibnd  27869  pntlemp  27886  ostth2lem2  27910  madebdayim  28193  no2indlesm  28259  no3inds  28263  istrkgc  28835  istrkgb  28836  istrkge  28838  trgcgrg  28897  tgcgr4  28913  isismt  28916  nbgr2vtx1edg  29850  nbuhgr2vtx1edgb  29852  uvtxval  29887  uvtxel  29888  uvtxel1  29896  uvtxusgrel  29903  cusgredg  29924  cplgr3v  29935  cplgrop  29937  usgredgsscusgredg  29959  isrgr  30059  isewlk  30102  iswlk  30110  iswwlks  30344  wlkiswwlks2  30383  isclwwlk  30494  clwlkclwwlklem1  30509  isconngr  30709  isconngr1  30710  isfrgr  30780  frgr1v  30791  nfrgr2v  30792  frgr3v  30795  1vwmgr  30796  3vfriswmgr  30798  3cyclfrgrrn1  30805  n4cyclfrgr  30811  isplig  30997  gidval  31033  vciOLD  31082  isvclem  31098  isnvlem  31131  lnoval  31273  ajfval  31330  isphg  31338  minvecolem3  31397  htth  31439  ressprs  33446  mntoval  33462  mgcoval  33466  fxpval  33645  isslmd  33682  resv1r  33819  mxidlval  33905  rprmval  33967  isufd  33991  vieta  34131  constrconj  34296  iscref  34395  ordtrest2NEW  34474  fmcncfil  34482  issiga  34663  isrnsiga  34664  isldsys  34708  ismeas  34751  carsgval  34855  issibf  34885  sitgfval  34893  signstfvneq0  35121  istrkg2d  35215  ispconn  35903  issconn  35906  txpconn  35912  cvxpconn  35922  cvmscbv  35938  iscvm  35939  cvmsdisj  35950  cvmsss2  35954  snmlval  36011  elmrsubrn  36200  ismfs  36229  mclsval  36243  fwddifnval  36844  weiunfrlem  37168  bj-ismoore  37940  pibp19  38251  pibp21  38252  poimirlem28  38480  cover2g  38564  seqpo  38595  incsequz2  38597  caushft  38609  ismtyval  38648  isass  38694  isexid  38695  elghomlem1OLD  38733  isrngo  38745  isrngod  38746  isgrpda  38803  rngohomval  38812  iscom2  38843  idlval  38861  pridlval  38881  maxidlval  38887  elrefrels3  39445  elcnvrefrels3  39461  eleqvrels3  39523  lflset  40030  islfld  40033  isopos  40151  isoml  40209  isatl  40270  iscvlat  40294  ishlat1  40323  psubspset  40715  lautset  41053  pautsetN  41069  ldilfset  41079  ltrnfset  41088  dilfsetN  41123  trnfsetN  41126  trnsetN  41127  trlfset  41131  tendofset  41729  tendoset  41730  dihffval  42201  lpolsetN  42453  hdmapfval  42798  hgmapfval  42857  sn-isghm  43617  aomclem8  44000  islnm  44016  clsk1independent  44984  gneispace2  45070  gneispaceel2  45082  gneispacess2  45084  caucvgbf  46415  ioodvbdlimc1lem1  46857  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  issal  47240  ismea  47377  isome  47420  chnerlem1  47808  tmachlem-agreesn  47873  iccpartiltu  48420  iccelpart  48431  isgrim  48896  isubgrgrim  48943  isgrlim  48996  usgrexmpl2trifr  49051  gpg5nbgr3star  49095  isupwlk  49150  iscllaw  49202  iscomlaw  49203  isasslaw  49205  zlidlring  49247  uzlidlring  49248  dmatALTval  49428  islininds  49474  lindslinindsimp2  49491  ldepsnlinc  49536  elbigo  49579  iscnrm3r  49972  isprsd  49979  lubeldm2d  49982  glbeldm2d  49983  nelsubc3lem  50094  ssccatid  50096  resccatlem  50097  upciclem1  50190  upfval  50200  upfval2  50201  upfval3  50202  oppcup3lem  50230  oppcup  50231  uptr2  50245  isthincd2lem2  50459  isthincd  50460  thincpropd  50466