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

Theorem raleqdv 2902
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 2896 . 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 1652   A.wral 2697
This theorem is referenced by:  raleqbidv  2908  raleqbidva  2910  cbvfo  6013  isoselem  6052  ofrfval  6304  issmo2  6602  smoeq  6603  frfi  7343  marypha1lem  7429  marypha1  7430  dfoi  7469  oieq2  7471  ordtypecbv  7475  ordtypelem2  7477  ordtypelem3  7478  ordtypelem9  7484  cantnfrescl  7621  wemapwe  7643  tcrank  7797  isacn  7914  pwsdompw  8073  isfin2  8163  isfin3ds  8198  isf33lem  8235  hsmexlem4  8298  zorn2lem6  8370  zorn2lem7  8371  zorn2g  8372  fpwwe2lem13  8506  uzsupss  10557  fzrevral2  11120  fzrevral3  11121  fzshftral  11122  expmulnbnd  11499  rexuz3  12140  rexuzre  12144  limsupgle  12259  rlim  12277  climconst  12325  rlimclim1  12327  climshftlem  12356  isercoll  12449  caucvgb  12461  serf0  12462  mertenslem1  12649  prmind2  13078  vdwlem10  13346  vdwlem13  13349  vdwnnlem2  13352  vdwnnlem3  13353  vdwnn  13354  ramval  13364  ramz  13381  isacs  13864  cidpropd  13924  monpropd  13951  isssc  14008  fullsubc  14035  funcpropd  14085  isfth  14099  fthpropd  14106  islat  14464  spwval  14645  mndpropd  14709  grpidpropd  14710  nmznsg  14972  ghmnsgima  15017  subgpgp  15219  sylow2blem3  15244  sylow3lem6  15254  efgsp1  15357  efgsres  15358  cmnpropd  15409  ablfac2  15635  rngpropd  15683  abvpropd  15918  lsspropd  16081  lmhmpropd  16133  lbspropd  16159  pj1lmhm  16160  assapropd  16374  znf1o  16820  phlpropd  16874  isclo  17139  perfopn  17237  lmfval  17284  lmconst  17313  cncnp  17332  iscnrm2  17390  ist0-2  17396  ist1-2  17399  ishaus2  17403  ordtt1  17431  subislly  17532  elpt  17592  elptr  17593  ptbasfi  17601  tx1stc  17670  xkococnlem  17679  fclscmp  18050  ufilcmp  18052  cnpfcf  18061  alexsubALTlem1  18066  alexsubALTlem2  18067  alexsubALTlem4  18069  tmdgsum2  18114  tsmsf1o  18162  ustval  18220  ucnval  18295  imasdsf1olem  18391  imasf1oxmet  18393  imasf1omet  18394  metss  18526  prdsxmslem2  18547  cnmpt2pc  18941  lebnumlem3  18976  ishtpy  18985  pi1coghm  19074  lmnn  19204  evthicc  19344  cniccbdd  19346  ovolicc2lem4  19404  0pledm  19553  cniccibl  19720  c1lip1  19869  dvivthlem1  19880  lhop1  19886  itgsubstlem  19920  dgrlem  20136  ulmshftlem  20293  ulm0  20295  ulmcau  20299  iblulm  20311  rlimcnp  20792  xrlimcnp  20795  fsumdvdsmul  20968  chtub  20984  2sqlem10  21146  dchrisum0flb  21192  pntpbnd1  21268  pntpbnd  21270  pntibndlem2  21273  pntibndlem3  21274  pntibnd  21275  pntlemi  21286  pntleme  21290  pntlem3  21291  pntlemp  21292  pntleml  21293  pnt3  21294  cusgra2v  21459  cusgra3v  21461  is2wlk  21553  constr1trl  21576  constr2wlk  21586  constr2trl  21587  redwlk  21594  usgrcyclnl2  21616  3v3e3cycl1  21619  constr3trllem2  21626  constr3trllem5  21629  4cycl4v4e  21641  4cycl4dv4e  21643  dfconngra1  21646  eupai  21677  eupatrl  21678  eupa0  21684  eupares  21685  eupap1  21686  isgrp2d  21811  isgrpda  21873  isass  21892  isrngod  21955  iscom2  21988  ubth  22363  lmxrge0  24325  sigaclcu3  24493  measval  24540  isrnmeas  24542  sitgval  24635  subfacp1lem3  24856  subfacp1lem5  24858  txpcon  24907  cvxpcon  24917  cvmscbv  24933  cvmsi  24940  cvmsval  24941  wfisg  25464  uzsinds  25471  omsinds  25474  frinsg  25500  wfrlem4  25514  brbtwn  25786  mblfinlem2  26191  ovoliunnfl  26194  voliunnfl  26196  volsupnfl  26197  cnicciblnc  26222  sdclem1  26384  fdc  26386  rrncmslem  26478  exidreslem  26489  exidresid  26491  kelac1  27076  gicabl  27178  islindf  27197  lindfmm  27212  islindf4  27223  islindf5  27224  lpirlnr  27236  psgnunilem3  27334  climsuse  27648  f12dfv  28011  f13dfv  28012  shwrd1  28161  shwrdsame  28163  shwrdssizelem1  28166  usgra2pthspth  28179  usgra2wlkspthlem1  28180  usgra2wlkspthlem2  28181  usgra2pthlem1  28184  usgra2pth  28185  frgra3v  28250  frgrawopreg1  28297  bnj1514  29286  pautsetN  30734  tendofset  31394  tendoset  31395  hdmap14lem13  32520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator