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

Theorem raleqdv 3057
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 3051 . 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 1398   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809
This theorem is referenced by:  raleqbidv  3065  raleqbidva  3067  raldifeq  3905  fveqressseq  6003  f12dfv  6154  f13dfv  6155  cbvfo  6167  isoselem  6212  ofrfval  6521  issmo2  7012  smoeq  7013  frfi  7757  marypha1lem  7885  marypha1  7886  dfoi  7928  oieq2  7930  ordtypecbv  7934  ordtypelem2  7936  ordtypelem3  7937  ordtypelem9  7943  wemapwe  8130  wemapweOLD  8131  tcrank  8293  isacn  8416  pwsdompw  8575  isfin2  8665  isfin3ds  8700  isf33lem  8737  hsmexlem4  8800  zorn2lem6  8872  zorn2lem7  8873  zorn2g  8874  fpwwe2lem13  9009  uzsupss  11175  fzrevral2  11768  fzrevral3  11769  fzshftral  11770  fzoshftral  11904  expmulnbnd  12283  eqs1  12613  swrdeq  12663  swrdspsleq  12668  2swrdeqwrdeq  12672  repswsymballbi  12746  cshw1  12784  wwlktovf1  12889  rexuz3  13266  rexuzre  13270  limsupgle  13385  rlim  13403  climconst  13451  rlimclim1  13453  climshftlem  13482  isercoll  13575  caucvgb  13587  serf0  13588  mertenslem1  13778  prmind2  14315  vdwlem10  14595  vdwlem13  14598  vdwnnlem2  14601  vdwnnlem3  14602  vdwnn  14603  ramval  14613  ramz  14630  isacs  15143  cidpropd  15201  monpropd  15228  isssc  15311  fullsubc  15341  funcpropd  15391  isfth  15405  fthpropd  15412  grpidpropd  16090  mndpropd  16148  nmznsg  16447  ghmnsgima  16492  symgextfo  16649  gsmsymgrfixlem1  16654  gsmsymgrfix  16655  fvcosymgeq  16656  gsmsymgreqlem2  16658  symgfixf1  16664  psgnunilem3  16723  subgpgp  16819  sylow2blem3  16844  sylow3lem6  16854  efgsp1  16957  efgsres  16958  cmnpropd  17009  telgsumfzs  17216  ablfac2  17338  ringpropd  17428  abvpropd  17689  lsspropd  17861  lmhmpropd  17917  lbspropd  17943  pj1lmhm  17944  assapropd  18174  znf1o  18766  psgndiflemB  18812  phlpropd  18866  islindf  19017  lindfmm  19032  islindf4  19043  islindf5  19044  scmatf1  19203  isclo  19758  perfopn  19856  lmfval  19903  lmconst  19932  cncnp  19951  iscnrm2  20009  ist0-2  20015  ist1-2  20018  ishaus2  20022  ordtt1  20050  subislly  20151  elpt  20242  elptr  20243  ptbasfi  20251  tx1stc  20320  xkococnlem  20329  fclscmp  20700  ufilcmp  20702  cnpfcf  20711  alexsubALTlem1  20716  alexsubALTlem2  20717  alexsubALTlem4  20719  tmdgsum2  20764  tsmsf1o  20816  ustval  20874  ucnval  20949  imasdsf1olem  21045  imasf1oxmet  21047  imasf1omet  21048  metss  21180  prdsxmslem2  21201  cnmpt2pc  21597  lebnumlem3  21632  ishtpy  21641  pi1coghm  21730  lmnn  21871  evthicc  22040  cniccbdd  22042  ovolicc2lem4  22100  0pledm  22249  cniccibl  22416  c1lip1  22567  dvivthlem1  22578  lhop1  22584  itgsubstlem  22618  dgrlem  22795  ulmshftlem  22953  ulm0  22955  ulmcau  22959  iblulm  22971  rlimcnp  23496  xrlimcnp  23499  fsumdvdsmul  23672  chtub  23688  2sqlem10  23850  dchrisum0flb  23896  pntpbnd1  23972  pntpbnd  23974  pntibndlem2  23977  pntibndlem3  23978  pntibnd  23979  pntlemi  23990  pntleme  23994  pntlem3  23995  pntlemp  23996  pntleml  23997  pnt3  23998  istrkgld  24058  trgcgrg  24110  isperp  24293  brbtwn  24407  cusgra2v  24667  cusgra3v  24669  uvtxnb  24702  is2wlk  24772  constr1trl  24795  constr2wlk  24805  constr2trl  24806  redwlk  24813  usgra2wlkspthlem1  24824  usgra2wlkspthlem2  24825  usgrcyclnl2  24846  3v3e3cycl1  24849  constr3trllem2  24856  constr3trllem5  24859  4cycl4v4e  24871  4cycl4dv4e  24873  dfconngra1  24876  wwlknimp  24892  wlkiswwlk1  24895  wlkiswwlk2lem4  24899  wwlkn0s  24910  vfwlkniswwlkn  24911  2wlkeq  24912  usg2wlkeq  24913  wwlknred  24928  wwlknext  24929  clwwlkn2  24980  clwwlknimp  24981  clwlkisclwwlklem2a1  24984  clwlkisclwwlklem2a  24990  clwlkisclwwlklem0  24993  clwwlkel  24998  clwwlkf  24999  wwlkext2clwwlk  25008  wwlksubclwwlk  25009  clwlkfclwwlk  25049  clwlkf1clwwlklem  25054  rusgranumwlkl1  25152  rusgra0edg  25160  eupai  25172  eupatrl  25173  eupa0  25179  eupares  25180  eupap1  25181  frgra3v  25207  frgrawopreg1  25255  extwwlkfablem2  25283  numclwwlkovf2ex  25291  isgrp2d  25438  isgrpda  25500  isass  25519  isrngod  25582  iscom2  25615  ubth  25990  acunirnmpt2  27730  acunirnmpt2f  27731  aciunf1  27733  lmxrge0  28172  sigaclcu3  28355  measval  28409  isrnmeas  28411  sitgval  28541  eulerpartlemsv3  28567  eulerpartlemo  28571  eulerpartlemn  28587  subfacp1lem3  28893  subfacp1lem5  28895  txpcon  28944  cvxpcon  28954  cvmscbv  28970  cvmsi  28977  cvmsval  28978  elmrsubrn  29147  wfisg  29532  uzsinds  29539  omsinds  29542  frinsg  29568  wfrlem4  29589  heicant  30292  mblfinlem3  30296  ovoliunnfl  30299  voliunnfl  30301  volsupnfl  30302  cnicciblnc  30329  sdclem1  30479  fdc  30481  rrncmslem  30571  exidreslem  30582  exidresid  30584  kelac1  31251  gicabl  31291  lpirlnr  31310  climsuse  31856  fourierdlem2  32133  fourierdlem3  32134  fourierdlem31  32162  fourierdlem47  32178  fourierdlem70  32201  fourierdlem71  32202  fourierdlem73  32204  fourierdlem80  32211  fourierdlem103  32234  fourierdlem104  32235  fourierdlem113  32244  pfxeq  32651  pfxsuffeqwrdeq  32653  pfx2  32659  2ffzoeq  32734  usgra2pthspth  32742  usgra2pthlem1  32744  usgra2pth  32745  linds0  33339  lindsrng01  33342  bnj1514  34539  pautsetN  36238  tendofset  36900  tendoset  36901  hdmap14lem13  38026  fiinfi  38190
  Copyright terms: Public domain W3C validator