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

Theorem raleqdv 2913
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 2907 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ps 
<-> 
A. x  e.  B  ps ) )
31, 2syl 16 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710
This theorem is referenced by:  raleqbidv  2921  raleqbidva  2923  raldifeq  3756  cbvfo  5980  isoselem  6019  ofrfval  6317  issmo2  6796  smoeq  6797  frfi  7545  marypha1lem  7671  marypha1  7672  dfoi  7713  oieq2  7715  ordtypecbv  7719  ordtypelem2  7721  ordtypelem3  7722  ordtypelem9  7728  cantnfrescl  7872  wemapwe  7916  wemapweOLD  7917  tcrank  8079  isacn  8202  pwsdompw  8361  isfin2  8451  isfin3ds  8486  isf33lem  8523  hsmexlem4  8586  zorn2lem6  8658  zorn2lem7  8659  zorn2g  8660  fpwwe2lem13  8796  uzsupss  10934  fzrevral2  11528  fzrevral3  11529  fzshftral  11530  fzoshftral  11619  expmulnbnd  11979  swrdeq  12323  swrdsymbeq  12324  swrdspsleq  12325  wrdeqswrdlsw  12326  2swrdeqwrdeq  12330  repswsymballbi  12401  cshw1  12439  rexuz3  12819  rexuzre  12823  limsupgle  12938  rlim  12956  climconst  13004  rlimclim1  13006  climshftlem  13035  isercoll  13128  caucvgb  13140  serf0  13141  mertenslem1  13326  prmind2  13756  vdwlem10  14033  vdwlem13  14036  vdwnnlem2  14039  vdwnnlem3  14040  vdwnn  14041  ramval  14051  ramz  14068  isacs  14571  cidpropd  14631  monpropd  14658  isssc  14715  fullsubc  14742  funcpropd  14792  isfth  14806  fthpropd  14813  mndpropd  15428  grpidpropd  15429  nmznsg  15704  ghmnsgima  15749  symgextfo  15906  gsmsymgrfixlem1  15911  gsmsymgrfix  15912  fvcosymgeq  15913  gsmsymgreqlem2  15915  symgfixf1  15922  psgnunilem3  15981  subgpgp  16075  sylow2blem3  16100  sylow3lem6  16110  efgsp1  16213  efgsres  16214  cmnpropd  16265  ablfac2  16563  rngpropd  16611  abvpropd  16850  lsspropd  17019  lmhmpropd  17075  lbspropd  17101  pj1lmhm  17102  assapropd  17319  znf1o  17825  psgndiflemB  17871  phlpropd  17925  islindf  18082  lindfmm  18097  islindf4  18108  islindf5  18109  isclo  18532  perfopn  18630  lmfval  18677  lmconst  18706  cncnp  18725  iscnrm2  18783  ist0-2  18789  ist1-2  18792  ishaus2  18796  ordtt1  18824  subislly  18926  elpt  18986  elptr  18987  ptbasfi  18995  tx1stc  19064  xkococnlem  19073  fclscmp  19444  ufilcmp  19446  cnpfcf  19455  alexsubALTlem1  19460  alexsubALTlem2  19461  alexsubALTlem4  19463  tmdgsum2  19508  tsmsf1o  19560  ustval  19618  ucnval  19693  imasdsf1olem  19789  imasf1oxmet  19791  imasf1omet  19792  metss  19924  prdsxmslem2  19945  cnmpt2pc  20341  lebnumlem3  20376  ishtpy  20385  pi1coghm  20474  lmnn  20615  evthicc  20784  cniccbdd  20786  ovolicc2lem4  20844  0pledm  20992  cniccibl  21159  c1lip1  21310  dvivthlem1  21321  lhop1  21327  itgsubstlem  21361  dgrlem  21581  ulmshftlem  21738  ulm0  21740  ulmcau  21744  iblulm  21756  rlimcnp  22243  xrlimcnp  22246  fsumdvdsmul  22419  chtub  22435  2sqlem10  22597  dchrisum0flb  22643  pntpbnd1  22719  pntpbnd  22721  pntibndlem2  22724  pntibndlem3  22725  pntibnd  22726  pntlemi  22737  pntleme  22741  pntlem3  22742  pntlemp  22743  pntleml  22744  pnt3  22745  trgcgrg  22847  brbtwn  22967  cusgra2v  23192  cusgra3v  23194  is2wlk  23286  constr1trl  23309  constr2wlk  23319  constr2trl  23320  redwlk  23327  usgrcyclnl2  23349  3v3e3cycl1  23352  constr3trllem2  23359  constr3trllem5  23362  4cycl4v4e  23374  4cycl4dv4e  23376  dfconngra1  23379  eupai  23410  eupatrl  23411  eupa0  23417  eupares  23418  eupap1  23419  isgrp2d  23544  isgrpda  23606  isass  23625  isrngod  23688  iscom2  23721  ubth  24096  lmxrge0  26235  sigaclcu3  26418  measval  26465  isrnmeas  26467  sitgval  26565  eulerpartlemsv3  26591  eulerpartlemo  26595  eulerpartlemn  26611  subfacp1lem3  26917  subfacp1lem5  26919  txpcon  26968  cvxpcon  26978  cvmscbv  26994  cvmsi  27001  cvmsval  27002  wfisg  27516  uzsinds  27523  omsinds  27526  frinsg  27552  wfrlem4  27573  heicant  28267  mblfinlem3  28271  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  cnicciblnc  28304  sdclem1  28480  fdc  28482  rrncmslem  28572  exidreslem  28583  exidresid  28585  kelac1  29258  gicabl  29296  lpirlnr  29315  climsuse  29624  f12dfv  29989  f13dfv  29990  2ffzoeq  30057  wwlktovf1  30095  uvtxnb  30121  2wlkeq  30131  usg2wlkeq  30132  usgra2pthspth  30138  usgra2wlkspthlem1  30139  usgra2wlkspthlem2  30140  usgra2pthlem1  30143  usgra2pth  30144  wwlknimp  30164  wlkiswwlk1  30167  wlkiswwlk2lem4  30171  vfwlkniswwlkn  30183  wwlknred  30198  wwlknext  30199  clwwlkn2  30281  clwwlknimp  30282  clwlkisclwwlklem2a1  30284  clwlkisclwwlklem2a  30290  clwlkisclwwlklem0  30293  clwwlkel  30298  clwwlkf  30299  wwlkext2clwwlk  30308  wwlksubclwwlk  30309  clwlkfclwwlk  30360  clwlkf1clwwlklem  30365  rusgranumwlkl1  30402  rusgra0edg  30416  frgra3v  30437  frgrawopreg1  30486  extwwlkfablem2  30514  numclwwlkovf2ex  30522  linds0  30705  lindsrng01  30708  bnj1514  31753  pautsetN  33312  tendofset  33972  tendoset  33973  hdmap14lem13  35098
  Copyright terms: Public domain W3C validator