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

Theorem raleqdv 3028
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 3022 . 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 187    = wceq 1437   A.wral 2771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776
This theorem is referenced by:  raleqbidv  3036  raleqbidva  3038  raleleqALT  3041  raldifeq  3887  wfisg  5434  fveqressseq  6033  f12dfv  6187  f13dfv  6188  cbvfo  6202  isoselem  6247  ofrfval  6553  omsinds  6725  wfrlem4  7050  issmo2  7079  smoeq  7080  frfi  7825  marypha1lem  7956  marypha1  7957  dfoi  8035  oieq2  8037  ordtypecbv  8041  ordtypelem2  8043  ordtypelem3  8044  ordtypelem9  8050  wemapwe  8210  tcrank  8363  isacn  8482  pwsdompw  8641  isfin2  8731  isfin3ds  8766  isf33lem  8803  hsmexlem4  8866  zorn2lem6  8938  zorn2lem7  8939  zorn2g  8940  fpwwe2lem13  9074  uzsupss  11263  fzrevral2  11887  fzrevral3  11888  fzshftral  11889  fzoshftral  12028  uzsinds  12205  expmulnbnd  12410  eqs1  12752  swrdeq  12802  swrdspsleq  12807  2swrdeqwrdeq  12811  repswsymballbi  12885  cshw1  12923  wwlktovf1  13032  rexuz3  13411  rexuzre  13415  limsupgle  13534  rlim  13558  climconst  13606  rlimclim1  13608  climshftlem  13637  isercoll  13730  caucvgb  13745  serf0  13746  mertenslem1  13939  lcmslefacOLD  14585  prmind2  14634  coprmprod  14677  coprmproddvds  14679  vdwlem10  14939  vdwlem13  14942  vdwnnlem2  14945  vdwnnlem3  14946  vdwnn  14947  ramval  14959  ramvalOLD  14960  ramz  14982  prmgaplcmlem1OLD  15011  prmordvdslcmsOLDOLD  15020  prmorlelcmsOLDOLD  15021  prmgaplem5  15024  isacs  15556  cidpropd  15614  monpropd  15641  isssc  15724  fullsubc  15754  funcpropd  15804  isfth  15818  fthpropd  15825  grpidpropd  16503  mndpropd  16561  nmznsg  16860  ghmnsgima  16905  symgextfo  17062  gsmsymgrfixlem1  17067  gsmsymgrfix  17068  fvcosymgeq  17069  gsmsymgreqlem2  17071  symgfixf1  17077  psgnunilem3  17136  subgpgp  17248  sylow2blem3  17273  sylow3lem6  17283  efgsp1  17386  efgsres  17387  cmnpropd  17438  telgsumfzs  17618  ablfac2  17721  ringpropd  17811  abvpropd  18069  lsspropd  18239  lmhmpropd  18295  lbspropd  18321  pj1lmhm  18322  assapropd  18550  znf1o  19120  psgndiflemB  19166  phlpropd  19220  islindf  19368  lindfmm  19383  islindf4  19394  islindf5  19395  scmatf1  19554  isclo  20101  perfopn  20199  lmfval  20246  lmconst  20275  cncnp  20294  iscnrm2  20352  ist0-2  20358  ist1-2  20361  ishaus2  20365  ordtt1  20393  subislly  20494  elpt  20585  elptr  20586  ptbasfi  20594  tx1stc  20663  xkococnlem  20672  fclscmp  21043  ufilcmp  21045  cnpfcf  21054  alexsubALTlem1  21060  alexsubALTlem2  21061  alexsubALTlem4  21063  tmdgsum2  21109  tsmsf1o  21157  ustval  21215  ucnval  21290  imasdsf1olem  21386  imasf1oxmet  21388  imasf1omet  21389  metss  21521  prdsxmslem2  21542  cnmpt2pc  21954  lebnumlem3  21989  lebnumlem3OLD  21992  ishtpy  22001  pi1coghm  22090  lmnn  22231  evthicc  22408  cniccbdd  22410  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  0pledm  22629  cniccibl  22796  c1lip1  22947  dvivthlem1  22958  lhop1  22964  itgsubstlem  22998  dgrlem  23181  ulmshftlem  23342  ulm0  23344  ulmcau  23348  iblulm  23360  rlimcnp  23889  xrlimcnp  23892  fsumdvdsmul  24122  chtub  24138  2sqlem10  24300  dchrisum0flb  24346  pntpbnd1  24422  pntpbnd  24424  pntibndlem2  24427  pntibndlem3  24428  pntibnd  24429  pntlemi  24440  pntleme  24444  pntlem3  24445  pntlemp  24446  pntleml  24447  pnt3  24448  istrkgld  24505  trgcgrg  24558  tgcgr4  24574  isperp  24755  brbtwn  24927  cusgra2v  25188  cusgra3v  25190  uvtxnb  25223  is2wlk  25293  constr1trl  25316  constr2wlk  25326  constr2trl  25327  redwlk  25334  usgra2wlkspthlem1  25345  usgra2wlkspthlem2  25346  usgrcyclnl2  25367  3v3e3cycl1  25370  constr3trllem2  25377  constr3trllem5  25380  4cycl4v4e  25392  4cycl4dv4e  25394  dfconngra1  25397  wwlknimp  25413  wlkiswwlk1  25416  wlkiswwlk2lem4  25420  wwlkn0s  25431  vfwlkniswwlkn  25432  2wlkeq  25433  usg2wlkeq  25434  wwlknred  25449  wwlknext  25450  clwwlkn2  25501  clwwlknimp  25502  clwlkisclwwlklem2a1  25505  clwlkisclwwlklem2a  25511  clwlkisclwwlklem0  25514  clwwlkel  25519  clwwlkf  25520  wwlkext2clwwlk  25529  wwlksubclwwlk  25530  clwlkfclwwlk  25570  clwlkf1clwwlklem  25575  rusgranumwlkl1  25673  rusgra0edg  25681  eupai  25693  eupatrl  25694  eupa0  25700  eupares  25701  eupap1  25702  frgra3v  25728  frgrawopreg1  25776  extwwlkfablem2  25804  numclwwlkovf2ex  25812  isgrp2d  25961  isgrpda  26023  isass  26042  isrngod  26105  iscom2  26138  ubth  26513  acunirnmpt2  28264  acunirnmpt2f  28265  aciunf1  28267  lmxrge0  28766  sigaclcu3  28952  measval  29028  isrnmeas  29030  sitgval  29173  eulerpartlemsv3  29202  eulerpartlemo  29206  eulerpartlemn  29222  bnj1514  29880  subfacp1lem3  29913  subfacp1lem5  29915  txpcon  29963  cvxpcon  29973  cvmscbv  29989  cvmsi  29996  cvmsval  29997  elmrsubrn  30166  frinsg  30490  poimirlem1  31905  poimirlem26  31930  poimirlem27  31931  poimirlem31  31935  poimirlem32  31936  heicant  31939  mblfinlem3  31943  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  cnicciblnc  31977  sdclem1  32036  fdc  32038  rrncmslem  32128  exidreslem  32139  exidresid  32141  pautsetN  33632  tendofset  34294  tendoset  34295  hdmap14lem13  35420  kelac1  35891  gicabl  35927  lpirlnr  35946  fiinfi  36147  raleqdOLD  37352  wessf1ornlem  37420  mccl  37618  climsuse  37627  fourierdlem2  37911  fourierdlem3  37912  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem47  37957  fourierdlem70  37980  fourierdlem71  37981  fourierdlem73  37983  fourierdlem80  37990  fourierdlem103  38013  fourierdlem104  38014  fourierdlem113  38023  etransclem48OLD  38087  etransclem48  38088  etransc  38089  issal  38096  ismea  38197  caragenval  38222  isome  38223  omessle  38227  iccpval  38599  iccpartigtl  38607  pfxeq  38815  pfxsuffeqwrdeq  38817  pfx2  38823  2ffzoeq  38918  usgruspgrb  39060  usgr1  39101  nbgr2vtx1edg  39183  nbuhgr2vtx1edgb  39185  nbgr0vtx  39189  nbgr1vtx  39191  uvtxa01vtx0  39228  cplgr1v  39254  cusgrexi  39264  usgra2pthspth  39285  usgra2pthlem1  39287  usgra2pth  39288  c0snmgmhm  39534  linds0  39880  lindsrng01  39883
  Copyright terms: Public domain W3C validator