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

Theorem raleqdv 3064
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 3058 . 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 1379   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819
This theorem is referenced by:  raleqbidv  3072  raleqbidva  3074  raldifeq  3916  f12dfv  6167  f13dfv  6168  cbvfo  6180  isoselem  6225  ofrfval  6532  issmo2  7020  smoeq  7021  frfi  7765  marypha1lem  7893  marypha1  7894  dfoi  7936  oieq2  7938  ordtypecbv  7942  ordtypelem2  7944  ordtypelem3  7945  ordtypelem9  7951  cantnfrescl  8095  wemapwe  8139  wemapweOLD  8140  tcrank  8302  isacn  8425  pwsdompw  8584  isfin2  8674  isfin3ds  8709  isf33lem  8746  hsmexlem4  8809  zorn2lem6  8881  zorn2lem7  8882  zorn2g  8883  fpwwe2lem13  9020  uzsupss  11174  fzrevral2  11763  fzrevral3  11764  fzshftral  11765  fzoshftral  11891  expmulnbnd  12266  swrdeq  12634  swrdsymbeq  12635  swrdspsleq  12636  wrdeqswrdlsw  12637  2swrdeqwrdeq  12641  repswsymballbi  12715  cshw1  12753  wwlktovf1  12858  rexuz3  13144  rexuzre  13148  limsupgle  13263  rlim  13281  climconst  13329  rlimclim1  13331  climshftlem  13360  isercoll  13453  caucvgb  13465  serf0  13466  mertenslem1  13656  prmind2  14087  vdwlem10  14367  vdwlem13  14370  vdwnnlem2  14373  vdwnnlem3  14374  vdwnn  14375  ramval  14385  ramz  14402  isacs  14906  cidpropd  14966  monpropd  14993  isssc  15050  fullsubc  15077  funcpropd  15127  isfth  15141  fthpropd  15148  mndpropd  15764  grpidpropd  15765  nmznsg  16050  ghmnsgima  16095  symgextfo  16252  gsmsymgrfixlem1  16257  gsmsymgrfix  16258  fvcosymgeq  16259  gsmsymgreqlem2  16261  symgfixf1  16268  psgnunilem3  16327  subgpgp  16423  sylow2blem3  16448  sylow3lem6  16458  efgsp1  16561  efgsres  16562  cmnpropd  16613  telgsumfzs  16821  ablfac2  16942  rngpropd  17031  abvpropd  17291  lsspropd  17463  lmhmpropd  17519  lbspropd  17545  pj1lmhm  17546  assapropd  17775  znf1o  18385  psgndiflemB  18431  phlpropd  18485  islindf  18642  lindfmm  18657  islindf4  18668  islindf5  18669  scmatf1  18828  isclo  19382  perfopn  19480  lmfval  19527  lmconst  19556  cncnp  19575  iscnrm2  19633  ist0-2  19639  ist1-2  19642  ishaus2  19646  ordtt1  19674  subislly  19776  elpt  19836  elptr  19837  ptbasfi  19845  tx1stc  19914  xkococnlem  19923  fclscmp  20294  ufilcmp  20296  cnpfcf  20305  alexsubALTlem1  20310  alexsubALTlem2  20311  alexsubALTlem4  20313  tmdgsum2  20358  tsmsf1o  20410  ustval  20468  ucnval  20543  imasdsf1olem  20639  imasf1oxmet  20641  imasf1omet  20642  metss  20774  prdsxmslem2  20795  cnmpt2pc  21191  lebnumlem3  21226  ishtpy  21235  pi1coghm  21324  lmnn  21465  evthicc  21634  cniccbdd  21636  ovolicc2lem4  21694  0pledm  21843  cniccibl  22010  c1lip1  22161  dvivthlem1  22172  lhop1  22178  itgsubstlem  22212  dgrlem  22389  ulmshftlem  22546  ulm0  22548  ulmcau  22552  iblulm  22564  rlimcnp  23051  xrlimcnp  23054  fsumdvdsmul  23227  chtub  23243  2sqlem10  23405  dchrisum0flb  23451  pntpbnd1  23527  pntpbnd  23529  pntibndlem2  23532  pntibndlem3  23533  pntibnd  23534  pntlemi  23545  pntleme  23549  pntlem3  23550  pntlemp  23551  pntleml  23552  pnt3  23553  trgcgrg  23662  isperp  23825  brbtwn  23906  cusgra2v  24166  cusgra3v  24168  uvtxnb  24201  is2wlk  24271  constr1trl  24294  constr2wlk  24304  constr2trl  24305  redwlk  24312  usgra2wlkspthlem1  24323  usgra2wlkspthlem2  24324  usgrcyclnl2  24345  3v3e3cycl1  24348  constr3trllem2  24355  constr3trllem5  24358  4cycl4v4e  24370  4cycl4dv4e  24372  dfconngra1  24375  wwlknimp  24391  wlkiswwlk1  24394  wlkiswwlk2lem4  24398  vfwlkniswwlkn  24410  2wlkeq  24411  usg2wlkeq  24412  wwlknred  24427  wwlknext  24428  clwwlkn2  24479  clwwlknimp  24480  clwlkisclwwlklem2a1  24483  clwlkisclwwlklem2a  24489  clwlkisclwwlklem0  24492  clwwlkel  24497  clwwlkf  24498  wwlkext2clwwlk  24507  wwlksubclwwlk  24508  clwlkfclwwlk  24548  clwlkf1clwwlklem  24553  rusgranumwlkl1  24651  rusgra0edg  24659  eupai  24671  eupatrl  24672  eupa0  24678  eupares  24679  eupap1  24680  frgra3v  24706  frgrawopreg1  24755  extwwlkfablem2  24783  numclwwlkovf2ex  24791  isgrp2d  24941  isgrpda  25003  isass  25022  isrngod  25085  iscom2  25118  ubth  25493  lmxrge0  27598  sigaclcu3  27790  measval  27837  isrnmeas  27839  sitgval  27942  eulerpartlemsv3  27968  eulerpartlemo  27972  eulerpartlemn  27988  subfacp1lem3  28294  subfacp1lem5  28296  txpcon  28345  cvxpcon  28355  cvmscbv  28371  cvmsi  28378  cvmsval  28379  wfisg  28894  uzsinds  28901  omsinds  28904  frinsg  28930  wfrlem4  28951  heicant  29654  mblfinlem3  29658  ovoliunnfl  29661  voliunnfl  29663  volsupnfl  29664  cnicciblnc  29691  sdclem1  29867  fdc  29869  rrncmslem  29959  exidreslem  29970  exidresid  29972  kelac1  30641  gicabl  30679  lpirlnr  30698  climsuse  31178  fourierdlem2  31437  fourierdlem3  31438  fourierdlem31  31466  fourierdlem47  31482  fourierdlem73  31508  fourierdlem103  31538  fourierdlem104  31539  fourierdlem113  31548  2ffzoeq  31836  usgra2pthspth  31846  usgra2pthlem1  31848  usgra2pth  31849  linds0  32165  lindsrng01  32168  bnj1514  33216  pautsetN  34912  tendofset  35572  tendoset  35573  hdmap14lem13  36698  fiinfi  36796
  Copyright terms: Public domain W3C validator