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

Theorem raleqdv 3005
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 2999 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ps 
<-> 
A. x  e.  B  ps ) )
31, 2syl 17 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754
This theorem is referenced by:  raleqbidv  3013  raleqbidva  3015  raleleqALT  3018  raldifeq  3869  wfisg  5438  fveqressseq  6046  f12dfv  6202  f13dfv  6203  cbvfo  6217  isoselem  6262  ofrfval  6571  omsinds  6743  wfrlem4  7070  issmo2  7099  smoeq  7100  frfi  7847  marypha1lem  7978  marypha1  7979  dfoi  8057  oieq2  8059  ordtypecbv  8063  ordtypelem2  8065  ordtypelem3  8066  ordtypelem9  8072  wemapwe  8233  tcrank  8386  isacn  8506  pwsdompw  8665  isfin2  8755  isfin3ds  8790  isf33lem  8827  hsmexlem4  8890  zorn2lem6  8962  zorn2lem7  8963  zorn2g  8964  fpwwe2lem13  9098  uzsupss  11290  fzrevral2  11915  fzrevral3  11916  fzshftral  11917  fzoshftral  12059  uzsinds  12237  expmulnbnd  12442  eqs1  12792  swrdeq  12843  swrdspsleq  12848  2swrdeqwrdeq  12852  repswsymballbi  12926  cshw1  12964  wwlktovf1  13087  rexuz3  13466  rexuzre  13470  limsupgle  13590  rlim  13614  climconst  13662  rlimclim1  13664  climshftlem  13693  isercoll  13786  caucvgb  13801  serf0  13802  mertenslem1  13995  lcmslefacOLD  14641  prmind2  14690  coprmprod  14733  coprmproddvds  14735  vdwlem10  14995  vdwlem13  14998  vdwnnlem2  15001  vdwnnlem3  15002  vdwnn  15003  ramval  15015  ramvalOLD  15016  ramz  15038  prmgaplcmlem1OLD  15067  prmordvdslcmsOLDOLD  15076  prmorlelcmsOLDOLD  15077  prmgaplem5  15080  isacs  15612  cidpropd  15670  monpropd  15697  isssc  15780  fullsubc  15810  funcpropd  15860  isfth  15874  fthpropd  15881  grpidpropd  16559  mndpropd  16617  nmznsg  16916  ghmnsgima  16961  symgextfo  17118  gsmsymgrfixlem1  17123  gsmsymgrfix  17124  fvcosymgeq  17125  gsmsymgreqlem2  17127  symgfixf1  17133  psgnunilem3  17192  subgpgp  17304  sylow2blem3  17329  sylow3lem6  17339  efgsp1  17442  efgsres  17443  cmnpropd  17494  telgsumfzs  17674  ablfac2  17777  ringpropd  17867  abvpropd  18125  lsspropd  18295  lmhmpropd  18351  lbspropd  18377  pj1lmhm  18378  assapropd  18606  znf1o  19177  psgndiflemB  19223  phlpropd  19277  islindf  19425  lindfmm  19440  islindf4  19451  islindf5  19452  scmatf1  19611  isclo  20158  perfopn  20256  lmfval  20303  lmconst  20332  cncnp  20351  iscnrm2  20409  ist0-2  20415  ist1-2  20418  ishaus2  20422  ordtt1  20450  subislly  20551  elpt  20642  elptr  20643  ptbasfi  20651  tx1stc  20720  xkococnlem  20729  fclscmp  21100  ufilcmp  21102  cnpfcf  21111  alexsubALTlem1  21117  alexsubALTlem2  21118  alexsubALTlem4  21120  tmdgsum2  21166  tsmsf1o  21214  ustval  21272  ucnval  21347  imasdsf1olem  21443  imasf1oxmet  21445  imasf1omet  21446  metss  21578  prdsxmslem2  21599  cnmpt2pc  22011  lebnumlem3  22046  lebnumlem3OLD  22049  ishtpy  22058  pi1coghm  22147  lmnn  22288  evthicc  22465  cniccbdd  22467  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  0pledm  22687  cniccibl  22854  c1lip1  23005  dvivthlem1  23016  lhop1  23022  itgsubstlem  23056  dgrlem  23239  ulmshftlem  23400  ulm0  23402  ulmcau  23406  iblulm  23418  rlimcnp  23947  xrlimcnp  23950  fsumdvdsmul  24180  chtub  24196  2sqlem10  24358  dchrisum0flb  24404  pntpbnd1  24480  pntpbnd  24482  pntibndlem2  24485  pntibndlem3  24486  pntibnd  24487  pntlemi  24498  pntleme  24502  pntlem3  24503  pntlemp  24504  pntleml  24505  pnt3  24506  istrkgld  24563  trgcgrg  24616  tgcgr4  24632  isperp  24813  brbtwn  24985  cusgra2v  25246  cusgra3v  25248  uvtxnb  25281  is2wlk  25351  constr1trl  25374  constr2wlk  25384  constr2trl  25385  redwlk  25392  usgra2wlkspthlem1  25403  usgra2wlkspthlem2  25404  usgrcyclnl2  25425  3v3e3cycl1  25428  constr3trllem2  25435  constr3trllem5  25438  4cycl4v4e  25450  4cycl4dv4e  25452  dfconngra1  25455  wwlknimp  25471  wlkiswwlk1  25474  wlkiswwlk2lem4  25478  wwlkn0s  25489  vfwlkniswwlkn  25490  2wlkeq  25491  usg2wlkeq  25492  wwlknred  25507  wwlknext  25508  clwwlkn2  25559  clwwlknimp  25560  clwlkisclwwlklem2a1  25563  clwlkisclwwlklem2a  25569  clwlkisclwwlklem0  25572  clwwlkel  25577  clwwlkf  25578  wwlkext2clwwlk  25587  wwlksubclwwlk  25588  clwlkfclwwlk  25628  clwlkf1clwwlklem  25633  rusgranumwlkl1  25731  rusgra0edg  25739  eupai  25751  eupatrl  25752  eupa0  25758  eupares  25759  eupap1  25760  frgra3v  25786  frgrawopreg1  25834  extwwlkfablem2  25862  numclwwlkovf2ex  25870  isgrp2d  26019  isgrpda  26081  isass  26100  isrngod  26163  iscom2  26196  ubth  26571  acunirnmpt2  28314  acunirnmpt2f  28315  aciunf1  28317  lmxrge0  28809  sigaclcu3  28995  measval  29071  isrnmeas  29073  sitgval  29215  eulerpartlemsv3  29244  eulerpartlemo  29248  eulerpartlemn  29264  bnj1514  29922  subfacp1lem3  29955  subfacp1lem5  29957  txpcon  30005  cvxpcon  30015  cvmscbv  30031  cvmsi  30038  cvmsval  30039  elmrsubrn  30208  frinsg  30533  poimirlem1  31987  poimirlem26  32012  poimirlem27  32013  poimirlem31  32017  poimirlem32  32018  heicant  32021  mblfinlem3  32025  ovoliunnfl  32028  voliunnfl  32030  volsupnfl  32031  cnicciblnc  32059  sdclem1  32118  fdc  32120  rrncmslem  32210  exidreslem  32221  exidresid  32223  pautsetN  33709  tendofset  34371  tendoset  34372  hdmap14lem13  35497  kelac1  35967  gicabl  36003  lpirlnr  36022  fiinfi  36223  raleqdOLD  37418  wessf1ornlem  37513  mccl  37764  climsuse  37773  fourierdlem2  38072  fourierdlem3  38073  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem47  38118  fourierdlem70  38141  fourierdlem71  38142  fourierdlem73  38144  fourierdlem80  38151  fourierdlem103  38174  fourierdlem104  38175  fourierdlem113  38184  etransclem48OLD  38248  etransclem48  38249  etransc  38250  issal  38276  ismea  38394  caragenval  38422  isome  38423  omessle  38427  iccpval  38864  iccpartigtl  38872  pfxeq  39082  pfxsuffeqwrdeq  39084  pfx2  39090  2ffzoeq  39202  usgruspgrb  39412  usgr1e  39466  nbgr2vtx1edg  39564  nbuhgr2vtx1edgb  39566  nbgr0vtx  39570  nbgr1vtx  39572  uvtxa01vtx0  39615  cplgr1v  39643  cusgrexi  39653  upgr2wlk  39811  red1wlk  39813  usgr2wlkneq  39884  pthdlem1  39888  uspgrn2crct  39922  1ewlk  39925  11wlkdlem4  39951  upgr3v3e3cycl  40017  upgr4cycl4dv4e  40022  dfconngr1  40025  isconngr1  40027  usgra2pthspth  40034  usgra2pthlem1  40036  usgra2pth  40037  c0snmgmhm  40283  linds0  40627  lindsrng01  40630
  Copyright terms: Public domain W3C validator