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

Theorem raleqdv 3415
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)
Hypothesis
Ref Expression
raleq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
raleqdv (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqdv
StepHypRef Expression
1 raleq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 raleq 3405 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1533  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143
This theorem is referenced by:  raleqbidvOLD  3423  raleqbidva  3425  raleleqALT  3428  raldifeq  4438  wfisg  6182  fveqressseq  6846  f12dfv  7029  f13dfv  7030  cbvfo  7044  isoselem  7093  ofrfval  7416  omsinds  7599  wfrlem4  7957  issmo2  7985  smoeq  7986  frfi  8762  marypha1lem  8896  marypha1  8897  dfoi  8974  oieq2  8976  ordtypecbv  8980  ordtypelem2  8982  ordtypelem3  8983  ordtypelem9  8989  wemapwe  9159  tcrank  9312  isacn  9469  pwsdompw  9625  isfin2  9715  isfin3ds  9750  isf33lem  9787  hsmexlem4  9850  zorn2lem6  9922  zorn2lem7  9923  zorn2g  9924  fpwwe2lem13  10063  uzsupss  12339  fzrevral2  12992  fzrevral3  12993  fzshftral  12994  fzoshftral  13153  uzsinds  13354  expmulnbnd  13595  eqs1  13965  swrdspsleq  14026  pfxeq  14057  pfxsuffeqwrdeq  14059  repswsymballbi  14141  cshw1  14183  pfx2  14308  wwlktovf1  14320  eqwrds3  14324  rexuz3  14707  rexuzre  14711  limsupgle  14833  rlim  14851  climconst  14899  rlimclim1  14901  climshftlem  14930  isercoll  15023  caucvgb  15035  serf0  15036  mertenslem1  15239  coprmprod  16004  coprmproddvds  16006  prmind2  16028  vdwlem10  16325  vdwlem13  16328  vdwnnlem2  16331  vdwnnlem3  16332  vdwnn  16333  ramval  16343  ramz  16360  prmgaplem5  16390  isacs  16921  cidpropd  16979  monpropd  17006  isssc  17089  fullsubc  17119  funcpropd  17169  isfth  17183  fthpropd  17190  grpidpropd  17871  mndpropd  17935  nmznsg  18319  ghmnsgima  18381  symgextfo  18549  gsmsymgrfixlem1  18554  gsmsymgrfix  18555  fvcosymgeq  18556  gsmsymgreqlem2  18558  symgfixf1  18564  psgnunilem3  18623  subgpgp  18721  sylow2blem3  18746  sylow3lem6  18756  efgsp1  18862  efgsres  18863  cmnpropd  18915  telgsumfzs  19108  ablfac2  19210  ringpropd  19331  abvpropd  19612  lsspropd  19788  lmhmpropd  19844  lbspropd  19870  pj1lmhm  19871  assapropd  20100  znf1o  20697  psgndiflemB  20743  phlpropd  20798  islindf  20955  lindfmm  20970  islindf4  20981  islindf5  20982  scmatf1  21139  isclo  21694  perfopn  21792  lmfval  21839  lmconst  21868  cncnp  21887  iscnrm2  21945  ist0-2  21951  ist1-2  21954  ishaus2  21958  ordtt1  21986  subislly  22088  elpt  22179  elptr  22180  ptbasfi  22188  tx1stc  22257  xkococnlem  22266  fclscmp  22637  ufilcmp  22639  cnpfcf  22648  alexsubALTlem1  22654  alexsubALTlem2  22655  alexsubALTlem4  22657  tmdgsum2  22703  tsmsf1o  22752  ustval  22810  ucnval  22885  imasdsf1olem  22982  imasf1oxmet  22984  imasf1omet  22985  metss  23117  prdsxmslem2  23138  cnmpopc  23531  lebnumlem3  23566  ishtpy  23575  pi1coghm  23664  lmnn  23865  evthicc  24059  cniccbdd  24061  ovolicc2lem4  24120  0pledm  24273  cniccibl  24440  c1lip1  24593  dvivthlem1  24604  lhop1  24610  itgsubstlem  24644  dgrlem  24818  ulmshftlem  24976  ulm0  24978  ulmcau  24982  iblulm  24994  rlimcnp  25542  xrlimcnp  25545  fsumdvdsmul  25771  chtub  25787  2sqlem10  26003  dchrisum0flb  26085  pntpbnd1  26161  pntpbnd  26163  pntibndlem2  26166  pntibndlem3  26167  pntibnd  26168  pntlemi  26179  pntleme  26183  pntlem3  26184  pntlemp  26185  pntleml  26186  pnt3  26187  istrkgld  26244  trgcgrg  26300  tgcgr4  26316  isperp  26497  brbtwn  26684  usgruspgrb  26965  usgr1e  27026  nbgr2vtx1edg  27131  nbuhgr2vtx1edgb  27133  nbgr0vtx  27137  nbgr1vtx  27139  uvtx01vtx  27178  cplgr1v  27211  cusgrexi  27224  1hevtxdg0  27286  wlkeq  27414  wlkl1loop  27418  uspgr2wlkeq  27426  upgr2wlk  27449  redwlk  27453  wlkp1lem8  27461  usgr2wlkneq  27536  usgr2trlncl  27540  usgr2pthlem  27543  usgr2pth  27544  pthdlem1  27546  uspgrn2crct  27585  crctcshwlkn0lem7  27593  crctcshwlkn0  27598  wwlknp  27620  wwlksn0s  27638  wlkiswwlks1  27644  wlkiswwlks2lem4  27649  wlkiswwlksupgr2  27654  wlknewwlksn  27664  wwlksnred  27669  wwlksnext  27670  rusgrnumwwlkl1  27746  clwwlkccatlem  27766  clwlkclwwlklem2a1  27769  clwlkclwwlklem2a  27775  clwlkclwwlklem3  27778  clwlkclwwlkf1lem3  27783  clwwlkn  27803  clwwlknp  27814  clwwlkinwwlk  27817  clwwlkn1  27818  clwwlkn2  27821  clwwlkel  27824  clwwlkf  27825  clwwlkwwlksb  27832  wwlksext2clwwlk  27835  wwlksubclwwlk  27836  clwwlknonex2  27887  1ewlk  27893  1wlkdlem4  27918  upgr3v3e3cycl  27958  upgr4cycl4dv4e  27963  dfconngr1  27966  isconngr1  27968  frgr3v  28053  frgrwopregasn  28094  frgrwopregbsn  28095  ubth  28649  acunirnmpt2  30404  acunirnmpt2f  30405  aciunf1  30407  fnpreimac  30415  lmxrge0  31195  sigaclcu3  31381  measval  31457  isrnmeas  31459  sitgval  31590  eulerpartlemsv3  31619  eulerpartlemo  31623  eulerpartlemn  31639  bnj1514  32335  subfacp1lem3  32429  subfacp1lem5  32431  txpconn  32479  cvxpconn  32489  cvmscbv  32505  cvmsi  32512  cvmsval  32513  satf  32600  sat1el2xp  32626  elmrsubrn  32767  frpoinsg  33081  frinsg  33087  frrlem4  33126  bj-raldifsn  34391  poimirlem1  34892  poimirlem26  34917  poimirlem27  34918  poimirlem31  34922  poimirlem32  34923  heicant  34926  mblfinlem3  34930  ovoliunnfl  34933  voliunnfl  34935  volsupnfl  34936  cnicciblnc  34962  sdclem1  35017  fdc  35019  rrncmslem  35109  isass  35123  exidreslem  35154  exidresid  35156  isrngod  35175  isgrpda  35232  iscom2  35272  pautsetN  37233  tendofset  37893  tendoset  37894  hdmap14lem13  39015  kelac1  39663  gicabl  39699  lpirlnr  39717  fiinfi  39932  clsk1independent  40396  scotteqd  40573  wessf1ornlem  41445  uzub  41705  mccl  41879  climsuse  41889  limsupmnfuzlem  42007  limsupmnfuz  42008  limsupre3uzlem  42016  limsupre3uz  42017  limsupreuz  42018  0cnv  42023  climuz  42025  lmbr3  42028  limsupgt  42059  liminflt  42086  xlimpnfxnegmnf  42095  xlimmnf  42122  xlimpnf  42123  xlimmnfmpt  42124  xlimpnfmpt  42125  dfxlim2  42129  fourierdlem2  42395  fourierdlem3  42396  fourierdlem31  42424  fourierdlem47  42439  fourierdlem70  42462  fourierdlem71  42463  fourierdlem73  42465  fourierdlem80  42472  fourierdlem103  42495  fourierdlem104  42496  fourierdlem113  42505  etransclem48  42568  etransc  42569  caragenval  42776  omessle  42781  smfmullem2  43068  smfmul  43071  2ffzoeq  43529  iccpval  43576  iccpartigtl  43584  c0snmgmhm  44186  linds0  44521  lindsrng01  44524  rrx2line  44728
  Copyright terms: Public domain W3C validator