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

Theorem raleqdv 3332
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 3326 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wral 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100
This theorem is referenced by:  raleqbidv  3340  raleqbidva  3342  raleleqALT  3345  raldifeq  4251  wfisg  5925  fveqressseq  6574  f12dfv  6750  f13dfv  6751  cbvfo  6765  isoselem  6812  ofrfval  7132  omsinds  7311  wfrlem4  7650  wfrlem4OLD  7651  issmo2  7679  smoeq  7680  frfi  8441  marypha1lem  8575  marypha1  8576  dfoi  8652  oieq2  8654  ordtypecbv  8658  ordtypelem2  8660  ordtypelem3  8661  ordtypelem9  8667  wemapwe  8838  tcrank  8991  isacn  9147  pwsdompw  9308  isfin2  9398  isfin3ds  9433  isf33lem  9470  hsmexlem4  9533  zorn2lem6  9605  zorn2lem7  9606  zorn2g  9607  fpwwe2lem13  9746  uzsupss  11995  fzrevral2  12645  fzrevral3  12646  fzshftral  12647  fzoshftral  12805  uzsinds  13006  expmulnbnd  13215  eqs1  13603  swrdeq  13664  swrdspsleq  13669  2swrdeqwrdeq  13673  repswsymballbi  13747  cshw1  13788  wwlktovf1  13921  eqwrds3  13925  rexuz3  14307  rexuzre  14311  limsupgle  14427  rlim  14445  climconst  14493  rlimclim1  14495  climshftlem  14524  isercoll  14617  caucvgb  14629  serf0  14630  mertenslem1  14833  coprmprod  15589  coprmproddvds  15591  prmind2  15612  vdwlem10  15907  vdwlem13  15910  vdwnnlem2  15913  vdwnnlem3  15914  vdwnn  15915  ramval  15925  ramz  15942  prmgaplem5  15972  isacs  16512  cidpropd  16570  monpropd  16597  isssc  16680  fullsubc  16710  funcpropd  16760  isfth  16774  fthpropd  16781  grpidpropd  17462  mndpropd  17517  nmznsg  17836  ghmnsgima  17882  symgextfo  18039  gsmsymgrfixlem1  18044  gsmsymgrfix  18045  fvcosymgeq  18046  gsmsymgreqlem2  18048  symgfixf1  18054  psgnunilem3  18113  subgpgp  18209  sylow2blem3  18234  sylow3lem6  18244  efgsp1  18347  efgsres  18348  cmnpropd  18399  telgsumfzs  18584  ablfac2  18686  ringpropd  18780  abvpropd  19042  lsspropd  19220  lmhmpropd  19276  lbspropd  19302  pj1lmhm  19303  assapropd  19532  znf1o  20103  psgndiflemB  20150  phlpropd  20206  islindf  20357  lindfmm  20372  islindf4  20383  islindf5  20384  scmatf1  20544  isclo  21101  perfopn  21199  lmfval  21246  lmconst  21275  cncnp  21294  iscnrm2  21352  ist0-2  21358  ist1-2  21361  ishaus2  21365  ordtt1  21393  subislly  21494  elpt  21585  elptr  21586  ptbasfi  21594  tx1stc  21663  xkococnlem  21672  fclscmp  22043  ufilcmp  22045  cnpfcf  22054  alexsubALTlem1  22060  alexsubALTlem2  22061  alexsubALTlem4  22063  tmdgsum2  22109  tsmsf1o  22157  ustval  22215  ucnval  22290  imasdsf1olem  22387  imasf1oxmet  22389  imasf1omet  22390  metss  22522  prdsxmslem2  22543  cnmpt2pc  22936  lebnumlem3  22971  ishtpy  22980  pi1coghm  23069  lmnn  23269  evthicc  23436  cniccbdd  23438  ovolicc2lem4  23497  0pledm  23650  cniccibl  23817  c1lip1  23970  dvivthlem1  23981  lhop1  23987  itgsubstlem  24021  dgrlem  24195  ulmshftlem  24353  ulm0  24355  ulmcau  24359  iblulm  24371  rlimcnp  24902  xrlimcnp  24905  fsumdvdsmul  25131  chtub  25147  2sqlem10  25363  dchrisum0flb  25409  pntpbnd1  25485  pntpbnd  25487  pntibndlem2  25490  pntibndlem3  25491  pntibnd  25492  pntlemi  25503  pntleme  25507  pntlem3  25508  pntlemp  25509  pntleml  25510  pnt3  25511  istrkgld  25568  trgcgrg  25620  tgcgr4  25636  isperp  25817  brbtwn  25989  usgruspgrb  26287  usgr1e  26349  nbgr2vtx1edg  26458  nbuhgr2vtx1edgb  26460  nbgr0vtx  26464  nbgr1vtx  26466  uvtx01vtx  26514  uvtxa01vtx0OLD  26516  cplgr1v  26550  cusgrexi  26563  1hevtxdg0  26625  wlkeq  26753  wlkl1loop  26758  uspgr2wlkeq  26766  upgr2wlk  26788  redwlk  26793  wlkp1lem8  26801  usgr2wlkneq  26876  usgr2trlncl  26880  usgr2pthlem  26883  usgr2pth  26884  pthdlem1  26886  uspgrn2crct  26925  crctcshwlkn0lem7  26933  crctcshwlkn0  26938  wwlknp  26960  wwlksn0s  26984  wlkiswwlks1  26990  wlkiswwlks2lem4  26995  wlkiswwlksupgr2  27000  wlknewwlksn  27010  wwlksnred  27025  wwlksnext  27026  rusgrnumwwlkl1  27106  clwwlkccatlem  27128  clwlkclwwlklem2a1  27131  clwlkclwwlklem2a  27137  clwlkclwwlklem3  27140  clwlkclwwlkf1lem3  27145  clwwlkn  27167  clwwlknp  27181  clwwlkinwwlk  27185  clwwlkn1  27186  clwwlkn2  27189  clwwlkel  27191  clwwlkf  27192  clwwlkwwlksb  27200  wwlksext2clwwlk  27203  wwlksext2clwwlkOLD  27204  wwlksubclwwlk  27205  clwlksfclwwlkOLD  27232  clwlksf1clwwlklemOLD  27238  clwwlknonex2  27274  1ewlk  27284  1wlkdlem4  27309  upgr3v3e3cycl  27349  upgr4cycl4dv4e  27354  dfconngr1  27357  isconngr1  27359  frgr3v  27446  frgrwopregasn  27487  frgrwopregbsn  27488  ubth  28054  acunirnmpt2  29784  acunirnmpt2f  29785  aciunf1  29787  lmxrge0  30320  sigaclcu3  30507  measval  30583  isrnmeas  30585  sitgval  30716  eulerpartlemsv3  30745  eulerpartlemo  30749  eulerpartlemn  30765  bnj1514  31451  subfacp1lem3  31484  subfacp1lem5  31486  txpconn  31534  cvxpconn  31544  cvmscbv  31560  cvmsi  31567  cvmsval  31568  elmrsubrn  31737  frpoinsg  32059  frinsg  32063  frrlem4  32101  bj-raldifsn  33362  poimirlem1  33720  poimirlem26  33745  poimirlem27  33746  poimirlem31  33750  poimirlem32  33751  heicant  33754  mblfinlem3  33758  ovoliunnfl  33761  voliunnfl  33763  volsupnfl  33764  cnicciblnc  33790  sdclem1  33847  fdc  33849  rrncmslem  33939  isass  33953  exidreslem  33984  exidresid  33986  isrngod  34005  isgrpda  34062  iscom2  34102  pautsetN  35875  tendofset  36536  tendoset  36537  hdmap14lem13  37658  kelac1  38131  gicabl  38167  lpirlnr  38185  fiinfi  38375  clsk1independent  38841  wessf1ornlem  39857  uzub  40134  mccl  40307  climsuse  40317  limsupmnfuzlem  40435  limsupmnfuz  40436  limsupre3uzlem  40444  limsupre3uz  40445  limsupreuz  40446  0cnv  40451  climuz  40453  lmbr3  40456  limsupgt  40487  liminflt  40514  xlimmnf  40544  xlimpnf  40545  xlimmnfmpt  40546  xlimpnfmpt  40547  dfxlim2  40551  fourierdlem2  40802  fourierdlem3  40803  fourierdlem31  40831  fourierdlem47  40846  fourierdlem70  40869  fourierdlem71  40870  fourierdlem73  40872  fourierdlem80  40879  fourierdlem103  40902  fourierdlem104  40903  fourierdlem113  40912  etransclem48  40975  etransc  40976  ismea  41144  caragenval  41186  omessle  41191  smfmullem2  41478  smfmul  41481  2ffzoeq  41910  iccpval  41923  iccpartigtl  41931  pfxeq  41976  pfxsuffeqwrdeq  41978  pfx2  41984  c0snmgmhm  42479  linds0  42819  lindsrng01  42822
  Copyright terms: Public domain W3C validator