Theorem raleqbidv 3338

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  rspc2vd  3899  frd  5612  f12dfv  7304  f13dfv  7305  knatar  7390  ofrfvalg  7725  fmpox  8103  ovmptssOLD  8130  frrlem4  8335  on2ind  8706  on3ind  8707  marypha1lem  9452  supeq123d  9469  oieq1  9533  acneq  10149  isfin1a  10397  fpwwe2cbv  10742  fpwwe2lem2  10744  fpwwecbv  10756  fpwwelem  10757  eltskg  10862  elgrug  10904  cau3lem  15551  rlim  15691  ello1  15711  elo1  15722  caurcvg2  15874  caucvgb  15876  fsum2dlem  15965  fsumcom2  15969  fprod2dlem  16176  fprodcom2  16180  pcfac  17106  vdwpc  17187  rami  17222  prmgaplem7  17264  prdsval  17655  ismre  17789  isacs2  17856  acsfiel  17857  iscat  17875  iscatd  17876  catidex  17877  catideu  17878  cidfval  17879  cidval  17880  catlid  17886  catrid  17887  comfeq  17909  catpropd  17912  monfval  17936  issubc  18039  fullsubc  18054  isfunc  18068  funcpropd  18106  isfull  18116  isfth  18120  fthpropd  18127  natfval  18153  initoval  18197  termoval  18198  isposd  18525  lubfval  18551  glbfval  18564  ischn  18810  chnind  18824  chnub  18825  ismgm  18846  mgmpropd  18858  ismgmd  18859  issstrmgm  18860  grpidval  18869  idressid  18891  gsumvalx  18894  gsumpropd  18896  gsumress  18900  ismgmhm  18914  resmgmhm  18929  issgrp  18938  sgrppropd  18949  ismnddef  18954  ismndd  18975  mndpropd  18980  ismhm  19009  resmhm  19045  isgrp  19179  grppropd  19191  isgrpd2e  19195  isnsg  19394  nmznsg  19407  isghm  19459  isga  19535  subgga  19544  gsmsymgrfix  19672  gsmsymgreq  19676  gexval  19822  ispgp  19836  isslw  19852  sylow2blem2  19865  efgval  19961  efgi  19963  efgsdm  19974  cmnpropd  20035  iscmnd  20038  submcmn2  20083  gsumzaddlem  20165  dmdprd  20244  dprdcntz  20254  isrng  20406  rngpropd  20426  issrg  20444  isring  20493  ringpropd  20549  isirred  20679  c0snmgmhm  20722  islring  20822  rrgval  20979  isdomn  20987  sdrgacs  21088  abvfval  21097  abvpropd  21122  islmod  21169  islmodd  21171  lmodprop2d  21229  lssset  21238  islmhm  21332  reslmhm  21357  lmhmpropd  21378  islbs  21381  prmidlval  21648  psgndiflemA  21937  isphl  21964  islindf  22148  islindf2  22150  lsslindf  22166  isassa  22194  isassad  22203  assapropd  22209  ltbval  22382  opsrval  22385  dmatval  22837  dmatcrng  22847  scmatcrng  22866  cpmat  23057  istopg  23243  restbas  23506  ordtrest2  23552  cnfval  23581  cnpfval  23582  ist0  23668  ist1  23669  ishaus  23670  iscnrm  23671  isnrm  23683  ist0-2  23692  ishaus2  23699  nrmsep3  23703  iscmp  23736  is1stc  23789  isptfin  23865  islocfin  23866  kgenval  23884  kgencn2  23906  txbas  23916  ptval  23919  dfac14  23967  isfil  24196  isufil  24252  isufl  24262  flfcntr  24392  ucnval  24625  iscusp  24647  prdsxmslem2  24878  tngngp3  25005  isnlm  25024  nmofval  25063  lebnumii  25317  iscau4  25630  iscmet  25635  iscmet3lem1  25642  iscmet3  25644  equivcmet  25668  ulmcaulem  26751  ulmcau  26752  fsumdvdscom  27542  dchrisumlem3  27848  pntibndlem2  27948  pntibnd  27950  pntlemp  27967  ostth2lem2  27991  madebdayim  28304  no2indlesm  28370  no3inds  28374  istrkgc  28946  istrkgb  28947  istrkge  28949  trgcgrg  29008  tgcgr4  29024  isismt  29027  nbgr2vtx1edg  29961  nbuhgr2vtx1edgb  29963  uvtxval  29998  uvtxel  29999  uvtxel1  30007  uvtxusgrel  30014  cusgredg  30035  cplgr3v  30046  cplgrop  30048  usgredgsscusgredg  30070  isrgr  30170  isewlk  30213  iswlk  30221  iswwlks  30455  wlkiswwlks2  30494  isclwwlk  30605  clwlkclwwlklem1  30620  isconngr  30820  isconngr1  30821  isfrgr  30891  frgr1v  30902  nfrgr2v  30903  frgr3v  30906  1vwmgr  30907  3vfriswmgr  30909  3cyclfrgrrn1  30916  n4cyclfrgr  30922  isplig  31108  gidval  31144  vciOLD  31193  isvclem  31209  isnvlem  31242  lnoval  31384  ajfval  31441  isphg  31449  minvecolem3  31508  htth  31550  ressprs  33597  mntoval  33613  mgcoval  33617  fxpval  33796  isslmd  33833  resv1r  33970  mxidlval  34056  rprmval  34118  isufd  34142  vieta  34282  constrconj  34447  iscref  34546  ordtrest2NEW  34625  fmcncfil  34633  issiga  34814  isrnsiga  34815  isldsys  34859  ismeas  34902  carsgval  35005  issibf  35035  sitgfval  35043  signstfvneq0  35271  istrkg2d  35365  ispconn  36155  issconn  36158  txpconn  36164  cvxpconn  36174  cvmscbv  36190  iscvm  36191  cvmsdisj  36202  cvmsss2  36206  snmlval  36263  elmrsubrn  36452  ismfs  36481  mclsval  36495  fwddifnval  37106  weiunfrlem  37430  bj-ismoore  38217  pibp19  38529  pibp21  38530  poimirlem28  38758  cover2g  38842  seqpo  38873  incsequz2  38875  caushft  38887  ismtyval  38926  isass  38972  isexid  38973  elghomlem1OLD  39011  isrngo  39023  isrngod  39024  isgrpda  39081  rngohomval  39090  iscom2  39121  idlval  39139  pridlval  39159  maxidlval  39165  elrefrels3  39723  elcnvrefrels3  39739  eleqvrels3  39801  lflset  40308  islfld  40311  isopos  40429  isoml  40487  isatl  40548  iscvlat  40572  ishlat1  40601  psubspset  40993  lautset  41331  pautsetN  41347  ldilfset  41357  ltrnfset  41366  dilfsetN  41401  trnfsetN  41404  trnsetN  41405  trlfset  41409  tendofset  42007  tendoset  42008  dihffval  42479  lpolsetN  42731  hdmapfval  43076  hgmapfval  43135  sn-isghm  43877  aomclem8  44256  islnm  44272  clsk1independent  45238  gneispace2  45324  gneispaceel2  45336  gneispacess2  45338  caucvgbf  46704  ioodvbdlimc1lem1  47146  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  issal  47529  ismea  47666  isome  47709  chnerlem1  48097  tmachlem-agreesn  48162  iccpartiltu  48709  iccelpart  48720  isgrim  49185  isubgrgrim  49232  isgrlim  49285  usgrexmpl2trifr  49340  gpg5nbgr3star  49384  isupwlk  49439  iscllaw  49491  iscomlaw  49492  isasslaw  49494  zlidlring  49536  uzlidlring  49537  dmatALTval  49717  islininds  49763  lindslinindsimp2  49780  ldepsnlinc  49825  elbigo  49868  iscnrm3r  50267  isprsd  50274  lubeldm2d  50277  glbeldm2d  50278  nelsubc3lem  50389  ssccatid  50391  resccatlem  50392  upciclem1  50487  upfval  50497  upfval2  50498  upfval3  50499  oppcup3lem  50527  oppcup  50528  uptr2  50542  isthincd2lem2  50775  isthincd  50776  thincpropd  50782