Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  raleqbidv Structured version   Visualization version   GIF version

Theorem raleqbidv 3354
 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 2175 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
StepHypRef Expression
1 raleqbidv.1 . . . 4 (𝜑𝐴 = 𝐵)
21eleq2d 2875 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
42, 3imbi12d 348 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
54ralbidv2 3160 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111 This theorem is referenced by:  raleqbi1dv  3356  rspc2vd  3877  f12dfv  7008  f13dfv  7009  knatar  7089  ofrfval  7397  fmpox  7747  ovmptss  7771  marypha1lem  8881  supeq123d  8898  oieq1  8960  acneq  9454  isfin1a  9703  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwecbv  10055  fpwwelem  10056  eltskg  10161  elgrug  10203  cau3lem  14706  rlim  14844  ello1  14864  elo1  14875  caurcvg2  15026  caucvgb  15028  fsum2dlem  15117  fsumcom2  15121  fprod2dlem  15326  fprodcom2  15330  pcfac  16225  vdwpc  16306  rami  16341  prmgaplem7  16383  prdsval  16720  ismre  16853  isacs2  16916  acsfiel  16917  iscat  16935  iscatd  16936  catidex  16937  catideu  16938  cidfval  16939  cidval  16940  catlid  16946  catrid  16947  comfeq  16968  catpropd  16971  monfval  16994  issubc  17097  fullsubc  17112  isfunc  17126  funcpropd  17162  isfull  17172  isfth  17176  fthpropd  17183  natfval  17208  initoval  17249  termoval  17250  isposd  17557  lubfval  17580  glbfval  17593  ismgm  17845  issstrmgm  17855  grpidval  17863  gsumvalx  17878  gsumpropd  17880  gsumress  17884  issgrp  17894  ismnddef  17905  ismndd  17925  mndpropd  17928  ismhm  17950  resmhm  17977  isgrp  18101  grppropd  18110  isgrpd2e  18114  isnsg  18299  nmznsg  18312  isghm  18350  isga  18413  subgga  18422  gsmsymgrfix  18548  gsmsymgreq  18552  gexval  18695  ispgp  18709  isslw  18725  sylow2blem2  18738  efgval  18835  efgi  18837  efgsdm  18848  cmnpropd  18908  iscmnd  18911  submcmn2  18952  gsumzaddlem  19034  dmdprd  19113  dprdcntz  19123  issrg  19250  isring  19294  ringpropd  19328  isirred  19445  sdrgacs  19573  abvfval  19582  abvpropd  19606  islmod  19631  islmodd  19633  lmodprop2d  19689  lssset  19698  islmhm  19792  reslmhm  19817  lmhmpropd  19838  islbs  19841  rrgval  20053  isdomn  20060  psgndiflemA  20290  isphl  20317  islindf  20501  islindf2  20503  lsslindf  20519  isassa  20545  isassad  20553  assapropd  20558  ltbval  20711  opsrval  20714  dmatval  21097  dmatcrng  21107  scmatcrng  21126  cpmat  21314  istopg  21500  restbas  21763  ordtrest2  21809  cnfval  21838  cnpfval  21839  ist0  21925  ist1  21926  ishaus  21927  iscnrm  21928  isnrm  21940  ist0-2  21949  ishaus2  21956  nrmsep3  21960  iscmp  21993  is1stc  22046  isptfin  22121  islocfin  22122  kgenval  22140  kgencn2  22162  txbas  22172  ptval  22175  dfac14  22223  isfil  22452  isufil  22508  isufl  22518  flfcntr  22648  ucnval  22883  iscusp  22905  prdsxmslem2  23136  tngngp3  23262  isnlm  23281  nmofval  23320  lebnumii  23571  iscau4  23883  iscmet  23888  iscmet3lem1  23895  iscmet3  23897  equivcmet  23921  ulmcaulem  24989  ulmcau  24990  fsumdvdscom  25770  dchrisumlem3  26075  pntibndlem2  26175  pntibnd  26177  pntlemp  26194  ostth2lem2  26218  trgcgrg  26309  tgcgr4  26325  isismt  26328  nbgr2vtx1edg  27140  nbuhgr2vtx1edgb  27142  uvtxval  27177  uvtxel  27178  uvtxel1  27186  uvtxusgrel  27193  cusgredg  27214  cplgr3v  27225  cplgrop  27227  usgredgsscusgredg  27249  isrgr  27349  isewlk  27392  iswlk  27400  iswwlks  27622  wlkiswwlks2  27661  isclwwlk  27769  clwlkclwwlklem1  27784  isconngr  27974  isconngr1  27975  isfrgr  28045  frgr1v  28056  nfrgr2v  28057  frgr3v  28060  1vwmgr  28061  3vfriswmgr  28063  3cyclfrgrrn1  28070  n4cyclfrgr  28076  isplig  28259  gidval  28295  vciOLD  28344  isvclem  28360  isnvlem  28393  lnoval  28535  ajfval  28592  isphg  28600  minvecolem3  28659  htth  28701  ressprs  30668  mntoval  30690  mgcoval  30694  isslmd  30880  resv1r  30961  prmidlval  31020  mxidlval  31041  isufd  31071  rprmval  31072  iscref  31197  ordtrest2NEW  31276  fmcncfil  31284  issiga  31481  isrnsiga  31482  isldsys  31525  ismeas  31568  carsgval  31671  issibf  31701  sitgfval  31709  signstfvneq0  31952  istrkg2d  32047  ispconn  32583  issconn  32586  txpconn  32592  cvxpconn  32602  cvmscbv  32618  iscvm  32619  cvmsdisj  32630  cvmsss2  32634  snmlval  32691  elmrsubrn  32880  ismfs  32909  mclsval  32923  frrlem4  33239  fwddifnval  33737  bj-ismoore  34520  pibp19  34831  pibp21  34832  poimirlem28  35085  cover2g  35153  seqpo  35185  incsequz2  35187  caushft  35199  ismtyval  35238  isass  35284  isexid  35285  elghomlem1OLD  35323  isrngo  35335  isrngod  35336  isgrpda  35393  rngohomval  35402  iscom2  35433  idlval  35451  pridlval  35471  maxidlval  35477  elrefrels3  35918  elcnvrefrels3  35931  eleqvrels3  35988  lflset  36355  islfld  36358  isopos  36476  isoml  36534  isatl  36595  iscvlat  36619  ishlat1  36648  psubspset  37040  lautset  37378  pautsetN  37394  ldilfset  37404  ltrnfset  37413  dilfsetN  37448  trnfsetN  37451  trnsetN  37452  trlfset  37456  tendofset  38054  tendoset  38055  dihffval  38526  lpolsetN  38778  hdmapfval  39123  hgmapfval  39182  aomclem8  40003  islnm  40019  clsk1independent  40747  gneispace2  40833  gneispaceel2  40845  gneispacess2  40847  ioodvbdlimc1lem1  42571  ioodvbdlimc1lem2  42572  ioodvbdlimc2lem  42574  issal  42954  ismea  43088  isome  43131  iccpartiltu  43937  iccelpart  43948  isomgr  44339  isupwlk  44362  mgmpropd  44393  ismgmd  44394  ismgmhm  44401  resmgmhm  44416  iscllaw  44447  iscomlaw  44448  isasslaw  44450  isrng  44498  c0snmgmhm  44536  zlidlring  44550  uzlidlring  44551  dmatALTval  44807  islininds  44853  lindslinindsimp2  44870  ldepsnlinc  44915  elbigo  44963
 Copyright terms: Public domain W3C validator