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

Theorem raleqdv 2755
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 2749 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ps 
<-> 
A. x  e.  B  ps ) )
31, 2syl 15 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   A.wral 2556
This theorem is referenced by:  raleqbidv  2761  raleqbidva  2763  cbvfo  5815  isoselem  5854  ofrfval  6102  issmo2  6382  smoeq  6383  frfi  7118  marypha1lem  7202  marypha1  7203  dfoi  7242  oieq2  7244  ordtypecbv  7248  ordtypelem2  7250  ordtypelem3  7251  ordtypelem9  7257  cantnfrescl  7394  wemapwe  7416  tcrank  7570  isacn  7687  pwsdompw  7846  isfin2  7936  isfin3ds  7971  isf33lem  8008  hsmexlem4  8071  zorn2lem6  8144  zorn2lem7  8145  zorn2g  8146  fpwwe2lem13  8280  uzsupss  10326  fzrevral2  10883  fzrevral3  10884  fzshftral  10885  expmulnbnd  11249  rexuz3  11848  rexuzre  11852  limsupgle  11967  rlim  11985  climconst  12033  rlimclim1  12035  climshftlem  12064  isercoll  12157  caucvgb  12168  serf0  12169  mertenslem1  12356  prmind2  12785  vdwlem10  13053  vdwlem13  13056  vdwnnlem2  13059  vdwnnlem3  13060  vdwnn  13061  ramval  13071  ramz  13088  isacs  13569  cidpropd  13629  monpropd  13656  isssc  13713  fullsubc  13740  funcpropd  13790  isfth  13804  fthpropd  13811  islat  14169  spwval  14350  mndpropd  14414  grpidpropd  14415  nmznsg  14677  ghmnsgima  14722  subgpgp  14924  sylow2blem3  14949  sylow3lem6  14959  efgsp1  15062  efgsres  15063  cmnpropd  15114  ablfac2  15340  rngpropd  15388  abvpropd  15623  lsspropd  15790  lmhmpropd  15842  lbspropd  15868  pj1lmhm  15869  assapropd  16083  znf1o  16521  phlpropd  16575  isclo  16840  perfopn  16931  lmfval  16978  lmconst  17007  cncnp  17025  iscnrm2  17082  ist0-2  17088  ist1-2  17091  ishaus2  17095  ordtt1  17123  subislly  17223  elpt  17283  elptr  17284  ptbasfi  17292  tx1stc  17360  xkococnlem  17369  fclscmp  17741  ufilcmp  17743  cnpfcf  17752  alexsubALTlem1  17757  alexsubALTlem2  17758  alexsubALTlem4  17760  tmdgsum2  17795  tsmsf1o  17843  imasdsf1olem  17953  imasf1oxmet  17955  imasf1omet  17956  metss  18070  prdsxmslem2  18091  cnmpt2pc  18442  lebnumlem3  18477  ishtpy  18486  pi1coghm  18575  lmnn  18705  evthicc  18835  cniccbdd  18837  ovolicc2lem4  18895  0pledm  19044  cniccibl  19211  c1lip1  19360  dvivthlem1  19371  lhop1  19377  itgsubstlem  19411  dgrlem  19627  ulmshftlem  19784  ulm0  19786  ulmcau  19788  iblulm  19799  rlimcnp  20276  xrlimcnp  20279  fsumdvdsmul  20451  chtub  20467  2sqlem10  20629  dchrisum0flb  20675  pntpbnd1  20751  pntpbnd  20753  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemi  20769  pntleme  20773  pntlem3  20774  pntlemp  20775  pntleml  20776  pnt3  20777  isgrp2d  20918  isgrpda  20980  isass  20999  isrngod  21062  iscom2  21095  ubth  21468  lmxrge0  23390  sigaclcu3  23498  measval  23544  isrnmeas  23546  subfacp1lem3  23728  subfacp1lem5  23730  txpcon  23778  cvxpcon  23788  cvmscbv  23804  cvmsi  23811  cvmsval  23812  eupai  23898  eupa0  23913  eupares  23914  eupap1  23915  wfisg  24280  uzsinds  24287  omsinds  24290  frinsg  24316  wfrlem4  24330  brbtwn  24599  ovoliunnfl  25001  cnicciblnc  25022  fatesg  25059  splint  25151  cnvref2  25169  mxlelt2  25368  mnlelt2  25369  rngounval2  25528  iscatOLD  25857  cati  25858  ismona  25912  islimcat  25979  isnword  26089  indcls2  26099  bisig0  26165  isibcg  26294  sdclem1  26556  fdc  26558  rrncmslem  26659  exidreslem  26670  exidresid  26672  kelac1  27264  gicabl  27366  islindf  27385  lindfmm  27400  islindf4  27411  islindf5  27412  lpirlnr  27424  psgnunilem3  27522  climsuse  27837  redwlk  28364  eupatrl  28385  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3trllem2  28397  constr3trllem5  28400  4cycl4v4e  28412  4cycl4dv4e  28414  frgra3v  28426  bnj1514  29409  pautsetN  30909  tendofset  31569  tendoset  31570  hdmap14lem13  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator