Theorem raleqbidv 3337

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2175, ax-11 2191, and ax-12 2212 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 1569   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

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

This theorem is used by:  rspc2vd  3900  frd  5617  f12dfv  7271  f13dfv  7272  knatar  7357  ofrfvalg  7684  fmpox  8062  ovmptss  8086  frrlem4  8284  on2ind  8653  on3ind  8654  marypha1lem  9391  supeq123d  9408  oieq1  9472  acneq  10034  isfin1a  10282  fpwwe2cbv  10621  fpwwe2lem2  10623  fpwwecbv  10635  fpwwelem  10636  eltskg  10741  elgrug  10783  cau3lem  15413  rlim  15553  ello1  15573  elo1  15584  caurcvg2  15736  caucvgb  15738  fsum2dlem  15828  fsumcom2  15832  fprod2dlem  16041  fprodcom2  16045  pcfac  16965  vdwpc  17046  rami  17081  prmgaplem7  17123  prdsval  17514  ismre  17648  isacs2  17715  acsfiel  17716  iscat  17734  iscatd  17735  catidex  17736  catideu  17737  cidfval  17738  cidval  17739  catlid  17745  catrid  17746  comfeq  17768  catpropd  17771  monfval  17795  issubc  17898  fullsubc  17913  isfunc  17927  funcpropd  17965  isfull  17975  isfth  17979  fthpropd  17986  natfval  18012  initoval  18056  termoval  18057  isposd  18384  lubfval  18410  glbfval  18423  ischn  18669  chnind  18683  chnub  18684  ismgm  18705  mgmpropd  18715  ismgmd  18716  issstrmgm  18717  grpidval  18725  gsumvalx  18740  gsumpropd  18742  gsumress  18746  ismgmhm  18760  resmgmhm  18775  issgrp  18784  sgrppropd  18795  ismnddef  18800  ismndd  18820  mndpropd  18823  ismhm  18849  resmhm  18885  isgrp  19012  grppropd  19024  isgrpd2e  19028  isnsg  19227  nmznsg  19240  isghm  19292  isga  19367  subgga  19376  gsmsymgrfix  19504  gsmsymgreq  19508  gexval  19654  ispgp  19668  isslw  19684  sylow2blem2  19697  efgval  19793  efgi  19795  efgsdm  19806  cmnpropd  19867  iscmnd  19870  submcmn2  19915  gsumzaddlem  19997  dmdprd  20076  dprdcntz  20086  isrng  20238  rngpropd  20258  issrg  20276  isring  20325  ringpropd  20378  isirred  20508  c0snmgmhm  20551  islring  20650  rrgval  20807  isdomn  20815  sdrgacs  20915  abvfval  20924  abvpropd  20949  islmod  20996  islmodd  20998  lmodprop2d  21056  lssset  21065  islmhm  21159  reslmhm  21184  lmhmpropd  21205  islbs  21208  prmidlval  21473  psgndiflemA  21762  isphl  21789  islindf  21973  islindf2  21975  lsslindf  21991  isassa  22017  isassad  22026  assapropd  22032  ltbval  22205  opsrval  22208  dmatval  22660  dmatcrng  22670  scmatcrng  22689  cpmat  22877  istopg  23063  restbas  23326  ordtrest2  23372  cnfval  23401  cnpfval  23402  ist0  23488  ist1  23489  ishaus  23490  iscnrm  23491  isnrm  23503  ist0-2  23512  ishaus2  23519  nrmsep3  23523  iscmp  23556  is1stc  23609  isptfin  23684  islocfin  23685  kgenval  23703  kgencn2  23725  txbas  23735  ptval  23738  dfac14  23786  isfil  24015  isufil  24071  isufl  24081  flfcntr  24211  ucnval  24444  iscusp  24466  prdsxmslem2  24697  tngngp3  24824  isnlm  24843  nmofval  24882  lebnumii  25136  iscau4  25449  iscmet  25454  iscmet3lem1  25461  iscmet3  25463  equivcmet  25487  ulmcaulem  26568  ulmcau  26569  fsumdvdscom  27360  dchrisumlem3  27666  pntibndlem2  27766  pntibnd  27768  pntlemp  27785  ostth2lem2  27809  madebdayim  28092  no2indlesm  28158  no3inds  28162  istrkgc  28734  istrkgb  28735  istrkge  28737  trgcgrg  28795  tgcgr4  28811  isismt  28814  nbgr2vtx1edg  29711  nbuhgr2vtx1edgb  29713  uvtxval  29748  uvtxel  29749  uvtxel1  29757  uvtxusgrel  29764  cusgredg  29785  cplgr3v  29796  cplgrop  29798  usgredgsscusgredg  29820  isrgr  29920  isewlk  29963  iswlk  29971  iswwlks  30196  wlkiswwlks2  30235  isclwwlk  30346  clwlkclwwlklem1  30361  isconngr  30551  isconngr1  30552  isfrgr  30622  frgr1v  30633  nfrgr2v  30634  frgr3v  30637  1vwmgr  30638  3vfriswmgr  30640  3cyclfrgrrn1  30647  n4cyclfrgr  30653  isplig  30839  gidval  30875  vciOLD  30924  isvclem  30940  isnvlem  30973  lnoval  31115  ajfval  31172  isphg  31180  minvecolem3  31239  htth  31281  ressprs  33295  mntoval  33311  mgcoval  33315  fxpval  33494  isslmd  33531  resv1r  33668  mxidlval  33753  rprmval  33815  isufd  33839  vieta  33979  constrconj  34144  iscref  34243  ordtrest2NEW  34322  fmcncfil  34330  issiga  34511  isrnsiga  34512  isldsys  34555  ismeas  34598  carsgval  34702  issibf  34732  sitgfval  34740  signstfvneq0  34968  istrkg2d  35062  ispconn  35723  issconn  35726  txpconn  35732  cvxpconn  35742  cvmscbv  35758  iscvm  35759  cvmsdisj  35770  cvmsss2  35774  snmlval  35831  elmrsubrn  36020  ismfs  36049  mclsval  36063  fwddifnval  36663  weiunfrlem  37003  bj-ismoore  37775  pibp19  38088  pibp21  38089  poimirlem28  38327  cover2g  38395  seqpo  38426  incsequz2  38428  caushft  38440  ismtyval  38479  isass  38525  isexid  38526  elghomlem1OLD  38564  isrngo  38576  isrngod  38577  isgrpda  38634  rngohomval  38643  iscom2  38674  idlval  38692  pridlval  38712  maxidlval  38718  elrefrels3  39276  elcnvrefrels3  39292  eleqvrels3  39354  lflset  39861  islfld  39864  isopos  39982  isoml  40040  isatl  40101  iscvlat  40125  ishlat1  40154  psubspset  40546  lautset  40884  pautsetN  40900  ldilfset  40910  ltrnfset  40919  dilfsetN  40954  trnfsetN  40957  trnsetN  40958  trlfset  40962  tendofset  41560  tendoset  41561  dihffval  42032  lpolsetN  42284  hdmapfval  42629  hgmapfval  42688  sn-isghm  43433  aomclem8  43816  islnm  43832  clsk1independent  44800  gneispace2  44886  gneispaceel2  44898  gneispacess2  44900  caucvgbf  46231  ioodvbdlimc1lem1  46673  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  issal  47056  ismea  47193  isome  47236  chnerlem1  47626  iccpartiltu  48199  iccelpart  48210  isgrim  48675  isubgrgrim  48722  isgrlim  48775  usgrexmpl2trifr  48830  gpg5nbgr3star  48874  isupwlk  48929  iscllaw  48982  iscomlaw  48983  isasslaw  48985  zlidlring  49027  uzlidlring  49028  dmatALTval  49208  islininds  49254  lindslinindsimp2  49271  ldepsnlinc  49316  elbigo  49359  iscnrm3r  49754  isprsd  49761  lubeldm2d  49764  glbeldm2d  49765  nelsubc3lem  49876  ssccatid  49878  resccatlem  49879  upciclem1  49972  upfval  49982  upfval2  49983  upfval3  49984  oppcup3lem  50012  oppcup  50013  uptr2  50027  isthincd2lem2  50241  isthincd  50242  thincpropd  50248