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

Theorem cbvralv 2892
Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)
Hypothesis
Ref Expression
cbvralv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvralv  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Distinct variable groups:    x, A    y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvralv
StepHypRef Expression
1 nfv 1626 . 2  |-  F/ y
ph
2 nfv 1626 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2888 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wral 2666
This theorem is referenced by:  cbvral2v  2900  cbvral3v  2902  reu7  3089  disjxun  4170  wereu2  4539  reusv3i  4689  dfwe2  4721  tfinds  4798  cnvpo  5369  f1mpt  5966  grprinvlem  6244  grprinvd  6245  tfrlem1  6595  tfrlem12  6609  rdglem1  6632  tz7.48lem  6657  nneneq  7249  marypha1lem  7396  supub  7420  suplub  7421  supmaxlem  7425  ordtypecbv  7442  ordtypelem3  7445  ordtypelem9  7451  wemaplem1  7471  brwdom3  7506  tcrank  7764  infxpenc2  7859  aceq1  7954  aceq2  7956  dfac5  7965  dfac9  7972  dfac12lem3  7981  kmlem12  7997  kmlem14  7999  cofsmo  8105  infpssrlem4  8142  isfin3ds  8165  isf32lem2  8190  isf32lem11  8199  isf33lem  8202  domtriomlem  8278  axdc3  8290  zorn2lem7  8338  zorn2g  8339  fpwwe2cbv  8461  fpwwecbv  8475  pwfseq  8495  axgroth6  8659  suprleub  9928  infmrgelb  9944  nnsub  9994  uzwo  10495  uzwoOLD  10496  ublbneg  10516  zsupss  10521  xrub  10846  monoord2  11309  faclbnd4lem4  11542  bccl  11568  hashbc  11657  wrdind  11746  cau3lem  12113  climmpt2  12322  caucvgrlem  12421  caurcvg2  12426  caucvgb  12428  fsum0diag2  12521  incexclem  12571  cvgrat  12615  mertenslem2  12617  mertens  12618  sqr2irr  12803  gcdcllem1  12966  prmind2  13045  prmpwdvds  13227  prmreclem5  13243  prmreclem6  13244  vdwlem7  13310  vdwlem10  13313  vdwlem13  13316  vdwnn  13321  ramcl  13352  isacs2  13833  catpropd  13890  spwmo  14613  gsumvalx  14729  issubg4  14916  isnsg2  14925  elnmz  14934  efgsdm  15317  pgpfac1lem5  15592  pgpfac1  15593  pgpfac  15597  ablfaclem3  15600  lbsextg  16189  evlslem2  16523  elcls3  17102  isclo2  17107  neiptopnei  17151  tgcn  17270  subbascn  17272  txcmplem2  17627  kqfvima  17715  kqt0lem  17721  isr0  17722  r0cld  17723  regr1lem2  17725  fbun  17825  flftg  17981  fclsbas  18006  alexsubALTlem2  18032  alexsubALTlem4  18034  ptcmplem4  18039  tsmsxplem1  18135  tsmsxp  18137  ustuqtop  18229  utopsnneip  18231  prdsxmslem2  18512  iscau4  19185  caucfil  19189  iscmet3  19199  bcthlem5  19234  bcth  19235  ovolicc2lem5  19370  uniioombllem6  19433  vitali  19458  ismbf3d  19499  itg1climres  19559  itg2seq  19587  itg2monolem1  19595  itg2mono  19598  rolle  19827  dvlipcn  19831  dvivthlem1  19845  mpfind  19918  ply1divex  20012  fta1g  20043  dgrco  20146  plydivex  20167  fta1  20178  vieta1  20182  ulmcaulem  20263  ulmcau  20264  abelthlem8  20308  wilth  20807  fta  20815  dchrelbas3  20975  2sqlem6  21106  2sqlem10  21111  dchrisumlem3  21138  dchrisum  21139  dchrmusumlema  21140  dchrvmasumlema  21147  dchrisum0lema  21161  pntibndlem3  21239  pntlem3  21256  pntleml  21258  pnt3  21259  ostth2lem2  21281  ostth  21286  cusgrafilem2  21442  grpoideu  21750  ubthlem3  22327  adjsym  23289  lnopunilem1  23466  elunop2  23469  lnophm  23475  cnlnadjlem5  23527  mdbr3  23753  mdbr4  23754  dmdbr3  23761  dmdbr4  23762  mddmd2  23765  toslub  24144  tosglb  24145  lmdvg  24291  esumcvg  24429  derangenlem  24810  subfacp1lem6  24824  subfacp1  24825  rescon  24886  cvmscbv  24898  untangtr  25116  dedekind  25140  dfon2lem3  25355  dfon2lem7  25359  cbvsetlike  25395  wfrlem1  25470  tfr3ALT  25493  frrlem1  25495  axcontlem1  25807  axcontlem6  25812  bpolyval  25999  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  mbfresfi  26152  nn0prpwlem  26215  neibastop3  26281  fnemeet2  26286  upixp  26321  sdclem2  26336  fdc  26339  mettrifi  26353  heiborlem5  26414  heiborlem10  26419  heibor  26420  bfp  26423  mzpclval  26672  dford3lem1  26987  fnwe2lem1  27015  aomclem3  27021  aomclem4  27022  aomclem8  27027  dfac11  27028  hbtlem5  27200  psgnunilem5  27285  psgnunilem3  27287  fnchoice  27567  cncmpmax  27570  climsuse  27601  stoweidlem7  27623  stoweidlem15  27631  stoweidlem35  27651  wallispilem3  27683  bnj1185  28871  bnj1379  28908  bnj222  28960  bnj517  28962  bnj1450  29125  bnj1452  29127  bnj1463  29130  cdleme25cv  30840  cdleme40v  30951
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671
  Copyright terms: Public domain W3C validator