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

Theorem raleqdv 2742
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 2736 . 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 1623   A.wral 2543
This theorem is referenced by:  raleqbidv  2748  raleqbidva  2750  cbvfo  5799  isoselem  5838  ofrfval  6086  issmo2  6366  smoeq  6367  frfi  7102  marypha1lem  7186  marypha1  7187  dfoi  7226  oieq2  7228  ordtypecbv  7232  ordtypelem2  7234  ordtypelem3  7235  ordtypelem9  7241  cantnfrescl  7378  wemapwe  7400  tcrank  7554  isacn  7671  pwsdompw  7830  isfin2  7920  isfin3ds  7955  isf33lem  7992  hsmexlem4  8055  zorn2lem6  8128  zorn2lem7  8129  zorn2g  8130  fpwwe2lem13  8264  uzsupss  10310  fzrevral2  10867  fzrevral3  10868  fzshftral  10869  expmulnbnd  11233  rexuz3  11832  rexuzre  11836  limsupgle  11951  rlim  11969  climconst  12017  rlimclim1  12019  climshftlem  12048  isercoll  12141  caucvgb  12152  serf0  12153  mertenslem1  12340  prmind2  12769  vdwlem10  13037  vdwlem13  13040  vdwnnlem2  13043  vdwnnlem3  13044  vdwnn  13045  ramval  13055  ramz  13072  isacs  13553  cidpropd  13613  monpropd  13640  isssc  13697  fullsubc  13724  funcpropd  13774  isfth  13788  fthpropd  13795  islat  14153  spwval  14334  mndpropd  14398  grpidpropd  14399  nmznsg  14661  ghmnsgima  14706  subgpgp  14908  sylow2blem3  14933  sylow3lem6  14943  efgsp1  15046  efgsres  15047  cmnpropd  15098  ablfac2  15324  rngpropd  15372  abvpropd  15607  lsspropd  15774  lmhmpropd  15826  lbspropd  15852  pj1lmhm  15853  assapropd  16067  znf1o  16505  phlpropd  16559  isclo  16824  perfopn  16915  lmfval  16962  lmconst  16991  cncnp  17009  iscnrm2  17066  ist0-2  17072  ist1-2  17075  ishaus2  17079  ordtt1  17107  subislly  17207  elpt  17267  elptr  17268  ptbasfi  17276  tx1stc  17344  xkococnlem  17353  fclscmp  17725  ufilcmp  17727  cnpfcf  17736  alexsubALTlem1  17741  alexsubALTlem2  17742  alexsubALTlem4  17744  tmdgsum2  17779  tsmsf1o  17827  imasdsf1olem  17937  imasf1oxmet  17939  imasf1omet  17940  metss  18054  prdsxmslem2  18075  cnmpt2pc  18426  lebnumlem3  18461  ishtpy  18470  pi1coghm  18559  lmnn  18689  evthicc  18819  cniccbdd  18821  ovolicc2lem4  18879  0pledm  19028  cniccibl  19195  c1lip1  19344  dvivthlem1  19355  lhop1  19361  itgsubstlem  19395  dgrlem  19611  ulmshftlem  19768  ulm0  19770  ulmcau  19772  iblulm  19783  rlimcnp  20260  xrlimcnp  20263  fsumdvdsmul  20435  chtub  20451  2sqlem10  20613  dchrisum0flb  20659  pntpbnd1  20735  pntpbnd  20737  pntibndlem2  20740  pntibndlem3  20741  pntibnd  20742  pntlemi  20753  pntleme  20757  pntlem3  20758  pntlemp  20759  pntleml  20760  pnt3  20761  isgrp2d  20902  isgrpda  20964  isass  20983  isrngod  21046  iscom2  21079  ubth  21452  lmxrge0  23375  sigaclcu3  23483  measval  23529  isrnmeas  23531  subfacp1lem3  23713  subfacp1lem5  23715  txpcon  23763  cvxpcon  23773  cvmscbv  23789  cvmsi  23796  cvmsval  23797  eupai  23883  eupa0  23898  eupares  23899  eupap1  23900  wfisg  24209  uzsinds  24216  omsinds  24219  frinsg  24245  wfrlem4  24259  brbtwn  24527  fatesg  24956  splint  25048  cnvref2  25066  mxlelt2  25265  mnlelt2  25266  rngounval2  25425  iscatOLD  25754  cati  25755  ismona  25809  islimcat  25876  isnword  25986  indcls2  25996  bisig0  26062  isibcg  26191  sdclem1  26453  fdc  26455  rrncmslem  26556  exidreslem  26567  exidresid  26569  kelac1  27161  gicabl  27263  islindf  27282  lindfmm  27297  islindf4  27308  islindf5  27309  lpirlnr  27321  psgnunilem3  27419  climsuse  27734  frgra3v  28180  bnj1514  29093  pautsetN  30287  tendofset  30947  tendoset  30948  hdmap14lem13  32073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator