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

Theorem raleqbidv 3399
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2136, ax-11 2151, and ax-12 2167 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 2895 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
42, 3imbi12d 346 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
54ralbidv2 3192 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140
This theorem is referenced by:  raleqbi1dv  3401  rspc2vd  3929  f12dfv  7021  f13dfv  7022  knatar  7099  ofrfval  7406  fmpox  7754  ovmptss  7777  marypha1lem  8885  supeq123d  8902  oieq1  8964  acneq  9457  isfin1a  9702  fpwwe2cbv  10040  fpwwe2lem2  10042  fpwwecbv  10054  fpwwelem  10055  eltskg  10160  elgrug  10202  cau3lem  14702  rlim  14840  ello1  14860  elo1  14871  caurcvg2  15022  caucvgb  15024  fsum2dlem  15113  fsumcom2  15117  fprod2dlem  15322  fprodcom2  15326  pcfac  16223  vdwpc  16304  rami  16339  prmgaplem7  16381  prdsval  16716  ismre  16849  isacs2  16912  acsfiel  16913  iscat  16931  iscatd  16932  catidex  16933  catideu  16934  cidfval  16935  cidval  16936  catlid  16942  catrid  16943  comfeq  16964  catpropd  16967  monfval  16990  issubc  17093  fullsubc  17108  isfunc  17122  funcpropd  17158  isfull  17168  isfth  17172  fthpropd  17179  natfval  17204  initoval  17245  termoval  17246  isposd  17553  lubfval  17576  glbfval  17589  ismgm  17841  issstrmgm  17851  grpidval  17859  gsumvalx  17874  gsumpropd  17876  gsumress  17880  issgrp  17890  ismnddef  17901  ismndd  17921  mndpropd  17924  ismhm  17946  resmhm  17973  isgrp  18047  grppropd  18056  isgrpd2e  18060  isnsg  18245  nmznsg  18258  isghm  18296  isga  18359  subgga  18368  gsmsymgrfix  18485  gsmsymgreq  18489  gexval  18632  ispgp  18646  isslw  18662  sylow2blem2  18675  efgval  18772  efgi  18774  efgsdm  18785  cmnpropd  18845  iscmnd  18848  submcmn2  18888  gsumzaddlem  18970  dmdprd  19049  dprdcntz  19059  issrg  19186  isring  19230  ringpropd  19261  isirred  19378  sdrgacs  19509  abvfval  19518  abvpropd  19542  islmod  19567  islmodd  19569  lmodprop2d  19625  lssset  19634  islmhm  19728  reslmhm  19753  lmhmpropd  19774  islbs  19777  rrgval  19988  isdomn  19995  isassa  20016  isassad  20024  assapropd  20029  ltbval  20180  opsrval  20183  psgndiflemA  20673  isphl  20700  islindf  20884  islindf2  20886  lsslindf  20902  dmatval  21029  dmatcrng  21039  scmatcrng  21058  cpmat  21245  istopg  21431  restbas  21694  ordtrest2  21740  cnfval  21769  cnpfval  21770  ist0  21856  ist1  21857  ishaus  21858  iscnrm  21859  isnrm  21871  ist0-2  21880  ishaus2  21887  nrmsep3  21891  iscmp  21924  is1stc  21977  isptfin  22052  islocfin  22053  kgenval  22071  kgencn2  22093  txbas  22103  ptval  22106  dfac14  22154  isfil  22383  isufil  22439  isufl  22449  flfcntr  22579  ucnval  22813  iscusp  22835  prdsxmslem2  23066  tngngp3  23192  isnlm  23211  nmofval  23250  lebnumii  23497  iscau4  23809  iscmet  23814  iscmet3lem1  23821  iscmet3  23823  equivcmet  23847  ulmcaulem  24909  ulmcau  24910  fsumdvdscom  25689  dchrisumlem3  25994  pntibndlem2  26094  pntibnd  26096  pntlemp  26113  ostth2lem2  26137  trgcgrg  26228  tgcgr4  26244  isismt  26247  nbgr2vtx1edg  27059  nbuhgr2vtx1edgb  27061  uvtxval  27096  uvtxel  27097  uvtxel1  27105  uvtxusgrel  27112  cusgredg  27133  cplgr3v  27144  cplgrop  27146  usgredgsscusgredg  27168  isrgr  27268  isewlk  27311  iswlk  27319  iswwlks  27541  wlkiswwlks2  27580  isclwwlk  27689  clwlkclwwlklem1  27704  isconngr  27895  isconngr1  27896  isfrgr  27966  frgr1v  27977  nfrgr2v  27978  frgr3v  27981  1vwmgr  27982  3vfriswmgr  27984  3cyclfrgrrn1  27991  n4cyclfrgr  27997  isplig  28180  gidval  28216  vciOLD  28265  isvclem  28281  isnvlem  28314  lnoval  28456  ajfval  28513  isphg  28521  minvecolem3  28580  htth  28622  ressprs  30569  isslmd  30757  resv1r  30837  prmidlval  30873  iscref  31007  ordtrest2NEW  31065  fmcncfil  31073  issiga  31270  isrnsiga  31271  isldsys  31314  ismeas  31357  carsgval  31460  issibf  31490  sitgfval  31498  signstfvneq0  31741  istrkg2d  31836  ispconn  32367  issconn  32370  txpconn  32376  cvxpconn  32386  cvmscbv  32402  iscvm  32403  cvmsdisj  32414  cvmsss2  32418  snmlval  32475  elmrsubrn  32664  ismfs  32693  mclsval  32707  frrlem4  33023  fwddifnval  33521  bj-ismoore  34291  pibp19  34577  pibp21  34578  poimirlem28  34801  cover2g  34871  seqpo  34903  incsequz2  34905  caushft  34917  ismtyval  34959  isass  35005  isexid  35006  elghomlem1OLD  35044  isrngo  35056  isrngod  35057  isgrpda  35114  rngohomval  35123  iscom2  35154  idlval  35172  pridlval  35192  maxidlval  35198  elrefrels3  35638  elcnvrefrels3  35651  eleqvrels3  35708  lflset  36075  islfld  36078  isopos  36196  isoml  36254  isatl  36315  iscvlat  36339  ishlat1  36368  psubspset  36760  lautset  37098  pautsetN  37114  ldilfset  37124  ltrnfset  37133  dilfsetN  37168  trnfsetN  37171  trnsetN  37172  trlfset  37176  tendofset  37774  tendoset  37775  dihffval  38246  lpolsetN  38498  hdmapfval  38843  hgmapfval  38902  aomclem8  39539  islnm  39555  clsk1independent  40274  gneispace2  40360  gneispaceel2  40372  gneispacess2  40374  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  issal  42476  ismea  42610  isome  42653  iccpartiltu  43459  iccelpart  43470  isomgr  43865  isupwlk  43888  mgmpropd  43919  ismgmd  43920  ismgmhm  43927  resmgmhm  43942  iscllaw  44024  iscomlaw  44025  isasslaw  44027  isrng  44075  c0snmgmhm  44113  zlidlring  44127  uzlidlring  44128  dmatALTval  44383  islininds  44429  lindslinindsimp2  44446  ldepsnlinc  44491  elbigo  44539
  Copyright terms: Public domain W3C validator