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

Theorem raleqdv 2944
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 2938 . 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 1369   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2741
This theorem is referenced by:  raleqbidv  2952  raleqbidva  2954  raldifeq  3789  cbvfo  6014  isoselem  6053  ofrfval  6349  issmo2  6831  smoeq  6832  frfi  7578  marypha1lem  7704  marypha1  7705  dfoi  7746  oieq2  7748  ordtypecbv  7752  ordtypelem2  7754  ordtypelem3  7755  ordtypelem9  7761  cantnfrescl  7905  wemapwe  7949  wemapweOLD  7950  tcrank  8112  isacn  8235  pwsdompw  8394  isfin2  8484  isfin3ds  8519  isf33lem  8556  hsmexlem4  8619  zorn2lem6  8691  zorn2lem7  8692  zorn2g  8693  fpwwe2lem13  8830  uzsupss  10968  fzrevral2  11566  fzrevral3  11567  fzshftral  11568  fzoshftral  11657  expmulnbnd  12017  swrdeq  12361  swrdsymbeq  12362  swrdspsleq  12363  wrdeqswrdlsw  12364  2swrdeqwrdeq  12368  repswsymballbi  12439  cshw1  12477  rexuz3  12857  rexuzre  12861  limsupgle  12976  rlim  12994  climconst  13042  rlimclim1  13044  climshftlem  13073  isercoll  13166  caucvgb  13178  serf0  13179  mertenslem1  13365  prmind2  13795  vdwlem10  14072  vdwlem13  14075  vdwnnlem2  14078  vdwnnlem3  14079  vdwnn  14080  ramval  14090  ramz  14107  isacs  14610  cidpropd  14670  monpropd  14697  isssc  14754  fullsubc  14781  funcpropd  14831  isfth  14845  fthpropd  14852  mndpropd  15467  grpidpropd  15468  nmznsg  15746  ghmnsgima  15791  symgextfo  15948  gsmsymgrfixlem1  15953  gsmsymgrfix  15954  fvcosymgeq  15955  gsmsymgreqlem2  15957  symgfixf1  15964  psgnunilem3  16023  subgpgp  16117  sylow2blem3  16142  sylow3lem6  16152  efgsp1  16255  efgsres  16256  cmnpropd  16307  ablfac2  16612  rngpropd  16698  abvpropd  16949  lsspropd  17120  lmhmpropd  17176  lbspropd  17202  pj1lmhm  17203  assapropd  17420  znf1o  18006  psgndiflemB  18052  phlpropd  18106  islindf  18263  lindfmm  18278  islindf4  18289  islindf5  18290  isclo  18713  perfopn  18811  lmfval  18858  lmconst  18887  cncnp  18906  iscnrm2  18964  ist0-2  18970  ist1-2  18973  ishaus2  18977  ordtt1  19005  subislly  19107  elpt  19167  elptr  19168  ptbasfi  19176  tx1stc  19245  xkococnlem  19254  fclscmp  19625  ufilcmp  19627  cnpfcf  19636  alexsubALTlem1  19641  alexsubALTlem2  19642  alexsubALTlem4  19644  tmdgsum2  19689  tsmsf1o  19741  ustval  19799  ucnval  19874  imasdsf1olem  19970  imasf1oxmet  19972  imasf1omet  19973  metss  20105  prdsxmslem2  20126  cnmpt2pc  20522  lebnumlem3  20557  ishtpy  20566  pi1coghm  20655  lmnn  20796  evthicc  20965  cniccbdd  20967  ovolicc2lem4  21025  0pledm  21173  cniccibl  21340  c1lip1  21491  dvivthlem1  21502  lhop1  21508  itgsubstlem  21542  dgrlem  21719  ulmshftlem  21876  ulm0  21878  ulmcau  21882  iblulm  21894  rlimcnp  22381  xrlimcnp  22384  fsumdvdsmul  22557  chtub  22573  2sqlem10  22735  dchrisum0flb  22781  pntpbnd1  22857  pntpbnd  22859  pntibndlem2  22862  pntibndlem3  22863  pntibnd  22864  pntlemi  22875  pntleme  22879  pntlem3  22880  pntlemp  22881  pntleml  22882  pnt3  22883  trgcgrg  22989  isperp  23125  brbtwn  23167  cusgra2v  23392  cusgra3v  23394  is2wlk  23486  constr1trl  23509  constr2wlk  23519  constr2trl  23520  redwlk  23527  usgrcyclnl2  23549  3v3e3cycl1  23552  constr3trllem2  23559  constr3trllem5  23562  4cycl4v4e  23574  4cycl4dv4e  23576  dfconngra1  23579  eupai  23610  eupatrl  23611  eupa0  23617  eupares  23618  eupap1  23619  isgrp2d  23744  isgrpda  23806  isass  23825  isrngod  23888  iscom2  23921  ubth  24296  lmxrge0  26404  sigaclcu3  26587  measval  26634  isrnmeas  26636  sitgval  26740  eulerpartlemsv3  26766  eulerpartlemo  26770  eulerpartlemn  26786  subfacp1lem3  27092  subfacp1lem5  27094  txpcon  27143  cvxpcon  27153  cvmscbv  27169  cvmsi  27176  cvmsval  27177  wfisg  27692  uzsinds  27699  omsinds  27702  frinsg  27728  wfrlem4  27749  heicant  28452  mblfinlem3  28456  ovoliunnfl  28459  voliunnfl  28461  volsupnfl  28462  cnicciblnc  28489  sdclem1  28665  fdc  28667  rrncmslem  28757  exidreslem  28768  exidresid  28770  kelac1  29442  gicabl  29480  lpirlnr  29499  climsuse  29807  f12dfv  30172  f13dfv  30173  2ffzoeq  30240  wwlktovf1  30278  uvtxnb  30304  2wlkeq  30314  usg2wlkeq  30315  usgra2pthspth  30321  usgra2wlkspthlem1  30322  usgra2wlkspthlem2  30323  usgra2pthlem1  30326  usgra2pth  30327  wwlknimp  30347  wlkiswwlk1  30350  wlkiswwlk2lem4  30354  vfwlkniswwlkn  30366  wwlknred  30381  wwlknext  30382  clwwlkn2  30464  clwwlknimp  30465  clwlkisclwwlklem2a1  30467  clwlkisclwwlklem2a  30473  clwlkisclwwlklem0  30476  clwwlkel  30481  clwwlkf  30482  wwlkext2clwwlk  30491  wwlksubclwwlk  30492  clwlkfclwwlk  30543  clwlkf1clwwlklem  30548  rusgranumwlkl1  30585  rusgra0edg  30599  frgra3v  30620  frgrawopreg1  30669  extwwlkfablem2  30697  numclwwlkovf2ex  30705  telescfzgsum  30843  linds0  30996  lindsrng01  30999  bnj1514  32150  pautsetN  33838  tendofset  34498  tendoset  34499  hdmap14lem13  35624
  Copyright terms: Public domain W3C validator