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

Theorem raleqdv 2910
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 2904 . 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 set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   A.wral 2705
This theorem is referenced by:  raleqbidv  2916  raleqbidva  2918  cbvfo  6022  isoselem  6061  ofrfval  6313  issmo2  6611  smoeq  6612  frfi  7352  marypha1lem  7438  marypha1  7439  dfoi  7480  oieq2  7482  ordtypecbv  7486  ordtypelem2  7488  ordtypelem3  7489  ordtypelem9  7495  cantnfrescl  7632  wemapwe  7654  tcrank  7808  isacn  7925  pwsdompw  8084  isfin2  8174  isfin3ds  8209  isf33lem  8246  hsmexlem4  8309  zorn2lem6  8381  zorn2lem7  8382  zorn2g  8383  fpwwe2lem13  8517  uzsupss  10568  fzrevral2  11132  fzrevral3  11133  fzshftral  11134  expmulnbnd  11511  rexuz3  12152  rexuzre  12156  limsupgle  12271  rlim  12289  climconst  12337  rlimclim1  12339  climshftlem  12368  isercoll  12461  caucvgb  12473  serf0  12474  mertenslem1  12661  prmind2  13090  vdwlem10  13358  vdwlem13  13361  vdwnnlem2  13364  vdwnnlem3  13365  vdwnn  13366  ramval  13376  ramz  13393  isacs  13876  cidpropd  13936  monpropd  13963  isssc  14020  fullsubc  14047  funcpropd  14097  isfth  14111  fthpropd  14118  islat  14476  spwval  14657  mndpropd  14721  grpidpropd  14722  nmznsg  14984  ghmnsgima  15029  subgpgp  15231  sylow2blem3  15256  sylow3lem6  15266  efgsp1  15369  efgsres  15370  cmnpropd  15421  ablfac2  15647  rngpropd  15695  abvpropd  15930  lsspropd  16093  lmhmpropd  16145  lbspropd  16171  pj1lmhm  16172  assapropd  16386  znf1o  16832  phlpropd  16886  isclo  17151  perfopn  17249  lmfval  17296  lmconst  17325  cncnp  17344  iscnrm2  17402  ist0-2  17408  ist1-2  17411  ishaus2  17415  ordtt1  17443  subislly  17544  elpt  17604  elptr  17605  ptbasfi  17613  tx1stc  17682  xkococnlem  17691  fclscmp  18062  ufilcmp  18064  cnpfcf  18073  alexsubALTlem1  18078  alexsubALTlem2  18079  alexsubALTlem4  18081  tmdgsum2  18126  tsmsf1o  18174  ustval  18232  ucnval  18307  imasdsf1olem  18403  imasf1oxmet  18405  imasf1omet  18406  metss  18538  prdsxmslem2  18559  cnmpt2pc  18953  lebnumlem3  18988  ishtpy  18997  pi1coghm  19086  lmnn  19216  evthicc  19356  cniccbdd  19358  ovolicc2lem4  19416  0pledm  19565  cniccibl  19732  c1lip1  19881  dvivthlem1  19892  lhop1  19898  itgsubstlem  19932  dgrlem  20148  ulmshftlem  20305  ulm0  20307  ulmcau  20311  iblulm  20323  rlimcnp  20804  xrlimcnp  20807  fsumdvdsmul  20980  chtub  20996  2sqlem10  21158  dchrisum0flb  21204  pntpbnd1  21280  pntpbnd  21282  pntibndlem2  21285  pntibndlem3  21286  pntibnd  21287  pntlemi  21298  pntleme  21302  pntlem3  21303  pntlemp  21304  pntleml  21305  pnt3  21306  cusgra2v  21471  cusgra3v  21473  is2wlk  21565  constr1trl  21588  constr2wlk  21598  constr2trl  21599  redwlk  21606  usgrcyclnl2  21628  3v3e3cycl1  21631  constr3trllem2  21638  constr3trllem5  21641  4cycl4v4e  21653  4cycl4dv4e  21655  dfconngra1  21658  eupai  21689  eupatrl  21690  eupa0  21696  eupares  21697  eupap1  21698  isgrp2d  21823  isgrpda  21885  isass  21904  isrngod  21967  iscom2  22000  ubth  22375  lmxrge0  24337  sigaclcu3  24505  measval  24552  isrnmeas  24554  sitgval  24647  subfacp1lem3  24868  subfacp1lem5  24870  txpcon  24919  cvxpcon  24929  cvmscbv  24945  cvmsi  24952  cvmsval  24953  wfisg  25484  uzsinds  25491  omsinds  25494  frinsg  25520  wfrlem4  25541  brbtwn  25838  mblfinlem3  26245  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  cnicciblnc  26276  sdclem1  26447  fdc  26449  rrncmslem  26541  exidreslem  26552  exidresid  26554  kelac1  27138  gicabl  27240  islindf  27259  lindfmm  27274  islindf4  27285  islindf5  27286  lpirlnr  27298  psgnunilem3  27396  climsuse  27710  f12dfv  28080  f13dfv  28081  2ffzoeq  28140  swdeq  28196  cshw1  28275  cshwsame  28277  cshwssizelem1  28280  2wlkeq  28303  usg2wlkeq  28304  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usgra2pthlem1  28310  usgra2pth  28311  frgra3v  28392  frgrawopreg1  28439  bnj1514  29432  pautsetN  30895  tendofset  31555  tendoset  31556  hdmap14lem13  32681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710
  Copyright terms: Public domain W3C validator