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

Theorem raleqdv 3416
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 3406 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wral 3138
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ral 3143
This theorem is referenced by:  raleqbidvOLD  3424  raleqbidva  3426  raleleqALT  3429  raldifeq  4437  wfisg  6177  fveqressseq  6840  f12dfv  7021  f13dfv  7022  cbvfo  7036  isoselem  7083  ofrfval  7406  omsinds  7588  wfrlem4  7949  issmo2  7977  smoeq  7978  frfi  8752  marypha1lem  8886  marypha1  8887  dfoi  8964  oieq2  8966  ordtypecbv  8970  ordtypelem2  8972  ordtypelem3  8973  ordtypelem9  8979  wemapwe  9149  tcrank  9302  isacn  9459  pwsdompw  9615  isfin2  9705  isfin3ds  9740  isf33lem  9777  hsmexlem4  9840  zorn2lem6  9912  zorn2lem7  9913  zorn2g  9914  fpwwe2lem13  10053  uzsupss  12329  fzrevral2  12983  fzrevral3  12984  fzshftral  12985  fzoshftral  13144  uzsinds  13345  expmulnbnd  13586  eqs1  13956  swrdspsleq  14017  pfxeq  14048  pfxsuffeqwrdeq  14050  repswsymballbi  14132  cshw1  14174  pfx2  14299  wwlktovf1  14311  eqwrds3  14315  rexuz3  14698  rexuzre  14702  limsupgle  14824  rlim  14842  climconst  14890  rlimclim1  14892  climshftlem  14921  isercoll  15014  caucvgb  15026  serf0  15027  mertenslem1  15230  coprmprod  15995  coprmproddvds  15997  prmind2  16019  vdwlem10  16316  vdwlem13  16319  vdwnnlem2  16322  vdwnnlem3  16323  vdwnn  16324  ramval  16334  ramz  16351  prmgaplem5  16381  isacs  16912  cidpropd  16970  monpropd  16997  isssc  17080  fullsubc  17110  funcpropd  17160  isfth  17174  fthpropd  17181  grpidpropd  17862  mndpropd  17926  nmznsg  18260  ghmnsgima  18322  symgextfo  18481  gsmsymgrfixlem1  18486  gsmsymgrfix  18487  fvcosymgeq  18488  gsmsymgreqlem2  18490  symgfixf1  18496  psgnunilem3  18555  subgpgp  18653  sylow2blem3  18678  sylow3lem6  18688  efgsp1  18794  efgsres  18795  cmnpropd  18847  telgsumfzs  19040  ablfac2  19142  ringpropd  19263  abvpropd  19544  lsspropd  19720  lmhmpropd  19776  lbspropd  19802  pj1lmhm  19803  assapropd  20031  znf1o  20628  psgndiflemB  20674  phlpropd  20729  islindf  20886  lindfmm  20901  islindf4  20912  islindf5  20913  scmatf1  21070  isclo  21625  perfopn  21723  lmfval  21770  lmconst  21799  cncnp  21818  iscnrm2  21876  ist0-2  21882  ist1-2  21885  ishaus2  21889  ordtt1  21917  subislly  22019  elpt  22110  elptr  22111  ptbasfi  22119  tx1stc  22188  xkococnlem  22197  fclscmp  22568  ufilcmp  22570  cnpfcf  22579  alexsubALTlem1  22585  alexsubALTlem2  22586  alexsubALTlem4  22588  tmdgsum2  22634  tsmsf1o  22682  ustval  22740  ucnval  22815  imasdsf1olem  22912  imasf1oxmet  22914  imasf1omet  22915  metss  23047  prdsxmslem2  23068  cnmpopc  23461  lebnumlem3  23496  ishtpy  23505  pi1coghm  23594  lmnn  23795  evthicc  23989  cniccbdd  23991  ovolicc2lem4  24050  0pledm  24203  cniccibl  24370  c1lip1  24523  dvivthlem1  24534  lhop1  24540  itgsubstlem  24574  dgrlem  24748  ulmshftlem  24906  ulm0  24908  ulmcau  24912  iblulm  24924  rlimcnp  25471  xrlimcnp  25474  fsumdvdsmul  25700  chtub  25716  2sqlem10  25932  dchrisum0flb  26014  pntpbnd1  26090  pntpbnd  26092  pntibndlem2  26095  pntibndlem3  26096  pntibnd  26097  pntlemi  26108  pntleme  26112  pntlem3  26113  pntlemp  26114  pntleml  26115  pnt3  26116  istrkgld  26173  trgcgrg  26229  tgcgr4  26245  isperp  26426  brbtwn  26613  usgruspgrb  26894  usgr1e  26955  nbgr2vtx1edg  27060  nbuhgr2vtx1edgb  27062  nbgr0vtx  27066  nbgr1vtx  27068  uvtx01vtx  27107  cplgr1v  27140  cusgrexi  27153  1hevtxdg0  27215  wlkeq  27343  wlkl1loop  27347  uspgr2wlkeq  27355  upgr2wlk  27378  redwlk  27382  wlkp1lem8  27390  usgr2wlkneq  27465  usgr2trlncl  27469  usgr2pthlem  27472  usgr2pth  27473  pthdlem1  27475  uspgrn2crct  27514  crctcshwlkn0lem7  27522  crctcshwlkn0  27527  wwlknp  27549  wwlksn0s  27567  wlkiswwlks1  27573  wlkiswwlks2lem4  27578  wlkiswwlksupgr2  27583  wlknewwlksn  27593  wwlksnred  27598  wwlksnext  27599  rusgrnumwwlkl1  27675  clwwlkccatlem  27695  clwlkclwwlklem2a1  27698  clwlkclwwlklem2a  27704  clwlkclwwlklem3  27707  clwlkclwwlkf1lem3  27712  clwwlkn  27732  clwwlknp  27743  clwwlkinwwlk  27746  clwwlkn1  27747  clwwlkn2  27750  clwwlkel  27753  clwwlkf  27754  clwwlkwwlksb  27761  wwlksext2clwwlk  27764  wwlksubclwwlk  27765  clwwlknonex2  27816  1ewlk  27822  1wlkdlem4  27847  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  dfconngr1  27895  isconngr1  27897  frgr3v  27982  frgrwopregasn  28023  frgrwopregbsn  28024  ubth  28578  acunirnmpt2  30334  acunirnmpt2f  30335  aciunf1  30337  fnpreimac  30345  lmxrge0  31095  sigaclcu3  31281  measval  31357  isrnmeas  31359  sitgval  31490  eulerpartlemsv3  31519  eulerpartlemo  31523  eulerpartlemn  31539  bnj1514  32233  subfacp1lem3  32327  subfacp1lem5  32329  txpconn  32377  cvxpconn  32387  cvmscbv  32403  cvmsi  32410  cvmsval  32411  satf  32498  sat1el2xp  32524  elmrsubrn  32665  frpoinsg  32979  frinsg  32985  frrlem4  33024  bj-raldifsn  34287  poimirlem1  34775  poimirlem26  34800  poimirlem27  34801  poimirlem31  34805  poimirlem32  34806  heicant  34809  mblfinlem3  34813  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  cnicciblnc  34845  sdclem1  34901  fdc  34903  rrncmslem  34993  isass  35007  exidreslem  35038  exidresid  35040  isrngod  35059  isgrpda  35116  iscom2  35156  pautsetN  37116  tendofset  37776  tendoset  37777  hdmap14lem13  38898  kelac1  39543  gicabl  39579  lpirlnr  39597  fiinfi  39812  clsk1independent  40276  scotteqd  40453  wessf1ornlem  41325  uzub  41585  mccl  41759  climsuse  41769  limsupmnfuzlem  41887  limsupmnfuz  41888  limsupre3uzlem  41896  limsupre3uz  41897  limsupreuz  41898  0cnv  41903  climuz  41905  lmbr3  41908  limsupgt  41939  liminflt  41966  xlimpnfxnegmnf  41975  xlimmnf  42002  xlimpnf  42003  xlimmnfmpt  42004  xlimpnfmpt  42005  dfxlim2  42009  fourierdlem2  42275  fourierdlem3  42276  fourierdlem31  42304  fourierdlem47  42319  fourierdlem70  42342  fourierdlem71  42343  fourierdlem73  42345  fourierdlem80  42352  fourierdlem103  42375  fourierdlem104  42376  fourierdlem113  42385  etransclem48  42448  etransc  42449  caragenval  42656  omessle  42661  smfmullem2  42948  smfmul  42951  2ffzoeq  43409  iccpval  43422  iccpartigtl  43430  c0snmgmhm  44083  linds0  44418  lindsrng01  44421  rrx2line  44625
  Copyright terms: Public domain W3C validator