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

Theorem raleqdv 2870
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 2864 . 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 set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   A.wral 2666
This theorem is referenced by:  raleqbidv  2876  raleqbidva  2878  cbvfo  5981  isoselem  6020  ofrfval  6272  issmo2  6570  smoeq  6571  frfi  7311  marypha1lem  7396  marypha1  7397  dfoi  7436  oieq2  7438  ordtypecbv  7442  ordtypelem2  7444  ordtypelem3  7445  ordtypelem9  7451  cantnfrescl  7588  wemapwe  7610  tcrank  7764  isacn  7881  pwsdompw  8040  isfin2  8130  isfin3ds  8165  isf33lem  8202  hsmexlem4  8265  zorn2lem6  8337  zorn2lem7  8338  zorn2g  8339  fpwwe2lem13  8473  uzsupss  10524  fzrevral2  11087  fzrevral3  11088  fzshftral  11089  expmulnbnd  11466  rexuz3  12107  rexuzre  12111  limsupgle  12226  rlim  12244  climconst  12292  rlimclim1  12294  climshftlem  12323  isercoll  12416  caucvgb  12428  serf0  12429  mertenslem1  12616  prmind2  13045  vdwlem10  13313  vdwlem13  13316  vdwnnlem2  13319  vdwnnlem3  13320  vdwnn  13321  ramval  13331  ramz  13348  isacs  13831  cidpropd  13891  monpropd  13918  isssc  13975  fullsubc  14002  funcpropd  14052  isfth  14066  fthpropd  14073  islat  14431  spwval  14612  mndpropd  14676  grpidpropd  14677  nmznsg  14939  ghmnsgima  14984  subgpgp  15186  sylow2blem3  15211  sylow3lem6  15221  efgsp1  15324  efgsres  15325  cmnpropd  15376  ablfac2  15602  rngpropd  15650  abvpropd  15885  lsspropd  16048  lmhmpropd  16100  lbspropd  16126  pj1lmhm  16127  assapropd  16341  znf1o  16787  phlpropd  16841  isclo  17106  perfopn  17203  lmfval  17250  lmconst  17279  cncnp  17298  iscnrm2  17356  ist0-2  17362  ist1-2  17365  ishaus2  17369  ordtt1  17397  subislly  17497  elpt  17557  elptr  17558  ptbasfi  17566  tx1stc  17635  xkococnlem  17644  fclscmp  18015  ufilcmp  18017  cnpfcf  18026  alexsubALTlem1  18031  alexsubALTlem2  18032  alexsubALTlem4  18034  tmdgsum2  18079  tsmsf1o  18127  ustval  18185  ucnval  18260  imasdsf1olem  18356  imasf1oxmet  18358  imasf1omet  18359  metss  18491  prdsxmslem2  18512  cnmpt2pc  18906  lebnumlem3  18941  ishtpy  18950  pi1coghm  19039  lmnn  19169  evthicc  19309  cniccbdd  19311  ovolicc2lem4  19369  0pledm  19518  cniccibl  19685  c1lip1  19834  dvivthlem1  19845  lhop1  19851  itgsubstlem  19885  dgrlem  20101  ulmshftlem  20258  ulm0  20260  ulmcau  20264  iblulm  20276  rlimcnp  20757  xrlimcnp  20760  fsumdvdsmul  20933  chtub  20949  2sqlem10  21111  dchrisum0flb  21157  pntpbnd1  21233  pntpbnd  21235  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemi  21251  pntleme  21255  pntlem3  21256  pntlemp  21257  pntleml  21258  pnt3  21259  cusgra2v  21424  cusgra3v  21426  is2wlk  21518  constr1trl  21541  constr2wlk  21551  constr2trl  21552  redwlk  21559  usgrcyclnl2  21581  3v3e3cycl1  21584  constr3trllem2  21591  constr3trllem5  21594  4cycl4v4e  21606  4cycl4dv4e  21608  dfconngra1  21611  eupai  21642  eupatrl  21643  eupa0  21649  eupares  21650  eupap1  21651  isgrp2d  21776  isgrpda  21838  isass  21857  isrngod  21920  iscom2  21953  ubth  22328  lmxrge0  24290  sigaclcu3  24458  measval  24505  isrnmeas  24507  sitgval  24600  subfacp1lem3  24821  subfacp1lem5  24823  txpcon  24872  cvxpcon  24882  cvmscbv  24898  cvmsi  24905  cvmsval  24906  wfisg  25423  uzsinds  25430  omsinds  25433  frinsg  25459  wfrlem4  25473  brbtwn  25742  mblfinlem2  26144  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  cnicciblnc  26175  sdclem1  26337  fdc  26339  rrncmslem  26431  exidreslem  26442  exidresid  26444  kelac1  27029  gicabl  27131  islindf  27150  lindfmm  27165  islindf4  27176  islindf5  27177  lpirlnr  27189  psgnunilem3  27287  climsuse  27601  f12dfv  27961  f13dfv  27962  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  usgra2pth  28041  frgra3v  28106  frgrawopreg1  28153  bnj1514  29138  pautsetN  30580  tendofset  31240  tendoset  31241  hdmap14lem13  32366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671
  Copyright terms: Public domain W3C validator