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

Theorem raleqdv 3046
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 3040 . 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 1383   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798
This theorem is referenced by:  raleqbidv  3054  raleqbidva  3056  raldifeq  3903  fveqressseq  6012  f12dfv  6164  f13dfv  6165  cbvfo  6177  isoselem  6222  ofrfval  6533  issmo2  7022  smoeq  7023  frfi  7767  marypha1lem  7895  marypha1  7896  dfoi  7939  oieq2  7941  ordtypecbv  7945  ordtypelem2  7947  ordtypelem3  7948  ordtypelem9  7954  wemapwe  8142  wemapweOLD  8143  tcrank  8305  isacn  8428  pwsdompw  8587  isfin2  8677  isfin3ds  8712  isf33lem  8749  hsmexlem4  8812  zorn2lem6  8884  zorn2lem7  8885  zorn2g  8886  fpwwe2lem13  9023  uzsupss  11185  fzrevral2  11775  fzrevral3  11776  fzshftral  11777  fzoshftral  11905  expmulnbnd  12280  swrdeq  12653  swrdsymbeq  12654  swrdspsleq  12655  wrdeqswrdlsw  12656  2swrdeqwrdeq  12660  repswsymballbi  12734  cshw1  12772  wwlktovf1  12877  rexuz3  13163  rexuzre  13167  limsupgle  13282  rlim  13300  climconst  13348  rlimclim1  13350  climshftlem  13379  isercoll  13472  caucvgb  13484  serf0  13485  mertenslem1  13675  prmind2  14210  vdwlem10  14490  vdwlem13  14493  vdwnnlem2  14496  vdwnnlem3  14497  vdwnn  14498  ramval  14508  ramz  14525  isacs  15030  cidpropd  15087  monpropd  15114  isssc  15171  fullsubc  15198  funcpropd  15248  isfth  15262  fthpropd  15269  grpidpropd  15867  mndpropd  15925  nmznsg  16224  ghmnsgima  16269  symgextfo  16426  gsmsymgrfixlem1  16431  gsmsymgrfix  16432  fvcosymgeq  16433  gsmsymgreqlem2  16435  symgfixf1  16441  psgnunilem3  16500  subgpgp  16596  sylow2blem3  16621  sylow3lem6  16631  efgsp1  16734  efgsres  16735  cmnpropd  16786  telgsumfzs  16997  ablfac2  17119  ringpropd  17209  abvpropd  17470  lsspropd  17642  lmhmpropd  17698  lbspropd  17724  pj1lmhm  17725  assapropd  17955  znf1o  18568  psgndiflemB  18614  phlpropd  18668  islindf  18825  lindfmm  18840  islindf4  18851  islindf5  18852  scmatf1  19011  isclo  19566  perfopn  19664  lmfval  19711  lmconst  19740  cncnp  19759  iscnrm2  19817  ist0-2  19823  ist1-2  19826  ishaus2  19830  ordtt1  19858  subislly  19960  elpt  20051  elptr  20052  ptbasfi  20060  tx1stc  20129  xkococnlem  20138  fclscmp  20509  ufilcmp  20511  cnpfcf  20520  alexsubALTlem1  20525  alexsubALTlem2  20526  alexsubALTlem4  20528  tmdgsum2  20573  tsmsf1o  20625  ustval  20683  ucnval  20758  imasdsf1olem  20854  imasf1oxmet  20856  imasf1omet  20857  metss  20989  prdsxmslem2  21010  cnmpt2pc  21406  lebnumlem3  21441  ishtpy  21450  pi1coghm  21539  lmnn  21680  evthicc  21849  cniccbdd  21851  ovolicc2lem4  21909  0pledm  22058  cniccibl  22225  c1lip1  22376  dvivthlem1  22387  lhop1  22393  itgsubstlem  22427  dgrlem  22604  ulmshftlem  22762  ulm0  22764  ulmcau  22768  iblulm  22780  rlimcnp  23273  xrlimcnp  23276  fsumdvdsmul  23449  chtub  23465  2sqlem10  23627  dchrisum0flb  23673  pntpbnd1  23749  pntpbnd  23751  pntibndlem2  23754  pntibndlem3  23755  pntibnd  23756  pntlemi  23767  pntleme  23771  pntlem3  23772  pntlemp  23773  pntleml  23774  pnt3  23775  istrkgld  23835  trgcgrg  23884  isperp  24067  brbtwn  24180  cusgra2v  24440  cusgra3v  24442  uvtxnb  24475  is2wlk  24545  constr1trl  24568  constr2wlk  24578  constr2trl  24579  redwlk  24586  usgra2wlkspthlem1  24597  usgra2wlkspthlem2  24598  usgrcyclnl2  24619  3v3e3cycl1  24622  constr3trllem2  24629  constr3trllem5  24632  4cycl4v4e  24644  4cycl4dv4e  24646  dfconngra1  24649  wwlknimp  24665  wlkiswwlk1  24668  wlkiswwlk2lem4  24672  wwlkn0s  24683  vfwlkniswwlkn  24684  2wlkeq  24685  usg2wlkeq  24686  wwlknred  24701  wwlknext  24702  clwwlkn2  24753  clwwlknimp  24754  clwlkisclwwlklem2a1  24757  clwlkisclwwlklem2a  24763  clwlkisclwwlklem0  24766  clwwlkel  24771  clwwlkf  24772  wwlkext2clwwlk  24781  wwlksubclwwlk  24782  clwlkfclwwlk  24822  clwlkf1clwwlklem  24827  rusgranumwlkl1  24925  rusgra0edg  24933  eupai  24945  eupatrl  24946  eupa0  24952  eupares  24953  eupap1  24954  frgra3v  24980  frgrawopreg1  25028  extwwlkfablem2  25056  numclwwlkovf2ex  25064  isgrp2d  25215  isgrpda  25277  isass  25296  isrngod  25359  iscom2  25392  ubth  25767  lmxrge0  27912  sigaclcu3  28100  measval  28147  isrnmeas  28149  sitgval  28252  eulerpartlemsv3  28278  eulerpartlemo  28282  eulerpartlemn  28298  subfacp1lem3  28604  subfacp1lem5  28606  txpcon  28655  cvxpcon  28665  cvmscbv  28681  cvmsi  28688  cvmsval  28689  elmrsubrn  28858  wfisg  29265  uzsinds  29272  omsinds  29275  frinsg  29301  wfrlem4  29322  heicant  30025  mblfinlem3  30029  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  cnicciblnc  30062  sdclem1  30212  fdc  30214  rrncmslem  30304  exidreslem  30315  exidresid  30317  kelac1  30985  gicabl  31023  lpirlnr  31042  climsuse  31568  fourierdlem2  31845  fourierdlem3  31846  fourierdlem31  31874  fourierdlem47  31890  fourierdlem70  31913  fourierdlem71  31914  fourierdlem73  31916  fourierdlem80  31923  fourierdlem103  31946  fourierdlem104  31947  fourierdlem113  31956  2ffzoeq  32295  usgra2pthspth  32305  usgra2pthlem1  32307  usgra2pth  32308  linds0  32936  lindsrng01  32939  bnj1514  33987  pautsetN  35697  tendofset  36359  tendoset  36360  hdmap14lem13  37485  fiinfi  37596
  Copyright terms: Public domain W3C validator