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

Theorem raleqdv 3038
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)
Hypothesis
Ref Expression
raleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
raleqdv  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem raleqdv
StepHypRef Expression
1 raleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 raleq 3032 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ps 
<-> 
A. x  e.  B  ps ) )
31, 2syl 17 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787
This theorem is referenced by:  raleqbidv  3046  raleqbidva  3048  raldifeq  3891  wfisg  5434  fveqressseq  6033  f12dfv  6187  f13dfv  6188  cbvfo  6202  isoselem  6247  ofrfval  6553  omsinds  6725  wfrlem4  7047  issmo2  7076  smoeq  7077  frfi  7822  marypha1lem  7953  marypha1  7954  dfoi  8026  oieq2  8028  ordtypecbv  8032  ordtypelem2  8034  ordtypelem3  8035  ordtypelem9  8041  wemapwe  8201  tcrank  8354  isacn  8473  pwsdompw  8632  isfin2  8722  isfin3ds  8757  isf33lem  8794  hsmexlem4  8857  zorn2lem6  8929  zorn2lem7  8930  zorn2g  8931  fpwwe2lem13  9066  uzsupss  11256  fzrevral2  11878  fzrevral3  11879  fzshftral  11880  fzoshftral  12019  uzsinds  12196  expmulnbnd  12401  eqs1  12735  swrdeq  12785  swrdspsleq  12790  2swrdeqwrdeq  12794  repswsymballbi  12868  cshw1  12906  wwlktovf1  13011  rexuz3  13390  rexuzre  13394  limsupgle  13513  rlim  13537  climconst  13585  rlimclim1  13587  climshftlem  13616  isercoll  13709  caucvgb  13724  serf0  13725  mertenslem1  13918  lcmslefacOLD  14557  prmind2  14606  coprmprod  14649  coprmproddvds  14651  vdwlem10  14903  vdwlem13  14906  vdwnnlem2  14909  vdwnnlem3  14910  vdwnn  14911  ramval  14923  ramvalOLD  14924  ramz  14946  prmgaplcmlem1OLD  14975  prmordvdslcmsOLDOLD  14984  prmorlelcmsOLDOLD  14985  prmgaplem5  14988  isacs  15508  cidpropd  15566  monpropd  15593  isssc  15676  fullsubc  15706  funcpropd  15756  isfth  15770  fthpropd  15777  grpidpropd  16455  mndpropd  16513  nmznsg  16812  ghmnsgima  16857  symgextfo  17014  gsmsymgrfixlem1  17019  gsmsymgrfix  17020  fvcosymgeq  17021  gsmsymgreqlem2  17023  symgfixf1  17029  psgnunilem3  17088  subgpgp  17184  sylow2blem3  17209  sylow3lem6  17219  efgsp1  17322  efgsres  17323  cmnpropd  17374  telgsumfzs  17554  ablfac2  17657  ringpropd  17747  abvpropd  18005  lsspropd  18175  lmhmpropd  18231  lbspropd  18257  pj1lmhm  18258  assapropd  18486  znf1o  19053  psgndiflemB  19099  phlpropd  19153  islindf  19301  lindfmm  19316  islindf4  19327  islindf5  19328  scmatf1  19487  isclo  20034  perfopn  20132  lmfval  20179  lmconst  20208  cncnp  20227  iscnrm2  20285  ist0-2  20291  ist1-2  20294  ishaus2  20298  ordtt1  20326  subislly  20427  elpt  20518  elptr  20519  ptbasfi  20527  tx1stc  20596  xkococnlem  20605  fclscmp  20976  ufilcmp  20978  cnpfcf  20987  alexsubALTlem1  20993  alexsubALTlem2  20994  alexsubALTlem4  20996  tmdgsum2  21042  tsmsf1o  21090  ustval  21148  ucnval  21223  imasdsf1olem  21319  imasf1oxmet  21321  imasf1omet  21322  metss  21454  prdsxmslem2  21475  cnmpt2pc  21852  lebnumlem3  21887  ishtpy  21896  pi1coghm  21985  lmnn  22126  evthicc  22291  cniccbdd  22293  ovolicc2lem4  22351  0pledm  22508  cniccibl  22675  c1lip1  22826  dvivthlem1  22837  lhop1  22843  itgsubstlem  22877  dgrlem  23051  ulmshftlem  23209  ulm0  23211  ulmcau  23215  iblulm  23227  rlimcnp  23756  xrlimcnp  23759  fsumdvdsmul  23987  chtub  24003  2sqlem10  24165  dchrisum0flb  24211  pntpbnd1  24287  pntpbnd  24289  pntibndlem2  24292  pntibndlem3  24293  pntibnd  24294  pntlemi  24305  pntleme  24309  pntlem3  24310  pntlemp  24311  pntleml  24312  pnt3  24313  istrkgld  24370  trgcgrg  24422  isperp  24614  brbtwn  24775  cusgra2v  25035  cusgra3v  25037  uvtxnb  25070  is2wlk  25140  constr1trl  25163  constr2wlk  25173  constr2trl  25174  redwlk  25181  usgra2wlkspthlem1  25192  usgra2wlkspthlem2  25193  usgrcyclnl2  25214  3v3e3cycl1  25217  constr3trllem2  25224  constr3trllem5  25227  4cycl4v4e  25239  4cycl4dv4e  25241  dfconngra1  25244  wwlknimp  25260  wlkiswwlk1  25263  wlkiswwlk2lem4  25267  wwlkn0s  25278  vfwlkniswwlkn  25279  2wlkeq  25280  usg2wlkeq  25281  wwlknred  25296  wwlknext  25297  clwwlkn2  25348  clwwlknimp  25349  clwlkisclwwlklem2a1  25352  clwlkisclwwlklem2a  25358  clwlkisclwwlklem0  25361  clwwlkel  25366  clwwlkf  25367  wwlkext2clwwlk  25376  wwlksubclwwlk  25377  clwlkfclwwlk  25417  clwlkf1clwwlklem  25422  rusgranumwlkl1  25520  rusgra0edg  25528  eupai  25540  eupatrl  25541  eupa0  25547  eupares  25548  eupap1  25549  frgra3v  25575  frgrawopreg1  25623  extwwlkfablem2  25651  numclwwlkovf2ex  25659  isgrp2d  25808  isgrpda  25870  isass  25889  isrngod  25952  iscom2  25985  ubth  26360  acunirnmpt2  28102  acunirnmpt2f  28103  aciunf1  28105  lmxrge0  28597  sigaclcu3  28783  measval  28859  isrnmeas  28861  sitgval  28993  eulerpartlemsv3  29020  eulerpartlemo  29024  eulerpartlemn  29040  bnj1514  29660  subfacp1lem3  29693  subfacp1lem5  29695  txpcon  29743  cvxpcon  29753  cvmscbv  29769  cvmsi  29776  cvmsval  29777  elmrsubrn  29946  frinsg  30270  poimirlem1  31644  poimirlem26  31669  poimirlem27  31670  poimirlem31  31674  poimirlem32  31675  heicant  31678  mblfinlem3  31682  ovoliunnfl  31685  voliunnfl  31687  volsupnfl  31688  cnicciblnc  31716  sdclem1  31775  fdc  31777  rrncmslem  31867  exidreslem  31878  exidresid  31880  pautsetN  33371  tendofset  34033  tendoset  34034  hdmap14lem13  35159  kelac1  35626  gicabl  35662  lpirlnr  35681  fiinfi  35875  raleqdOLD  37018  wessf1ornlem  37081  mccl  37249  climsuse  37258  fourierdlem2  37539  fourierdlem3  37540  fourierdlem31  37568  fourierdlem47  37584  fourierdlem70  37607  fourierdlem71  37608  fourierdlem73  37610  fourierdlem80  37617  fourierdlem103  37640  fourierdlem104  37641  fourierdlem113  37650  etransclem48  37713  etransc  37714  issal  37721  ismea  37797  caragenval  37822  isome  37823  omessle  37827  iccpval  38118  iccpartigtl  38126  pfxeq  38334  pfxsuffeqwrdeq  38336  pfx2  38342  2ffzoeq  38412  usgra2pthspth  38420  usgra2pthlem1  38422  usgra2pth  38423  c0snmgmhm  38671  linds0  39017  lindsrng01  39020
  Copyright terms: Public domain W3C validator