Theorem cbvralv 2654

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

Step	Hyp	Ref	Expression
1		nfv 1508	. 2 |- F/ y ph
2		nfv 1508	. 2 |- F/ x ps
3		cbvralv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvral 2650	1 |- ( A. x e. A ph <-> A. y e. A ps )

Syntax hints:   -> wi 4   <-> wb 104   A.wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421

This theorem is referenced by:  cbvralvw  2658  cbvral2v  2665  cbvral3v  2667  reu7  2879  reusv3i  4380  omsinds  4535  cnvpom  5081  f1mpt  5672  grprinvlem  5965  grprinvd  5966  tfrlem1  6205  tfrlemiubacc  6227  tfrlemi1  6229  tfr1onlemubacc  6243  tfr1onlemaccex  6245  tfrcllembxssdm  6253  tfrcllemubacc  6256  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  rdgon  6283  frecfcllem  6301  frecsuclem  6303  nneneq  6751  fimax2gtrilemstep  6794  supubti  6886  suplubti  6887  finomni  7012  acfun  7063  ccfunen  7079  cauappcvgprlemladdrl  7465  caucvgprlemcl  7484  caucvgprlemladdrl  7486  caucvgsrlembound  7602  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  suplocsrlem  7616  peano5nnnn  7700  axcaucvglemres  7707  axpre-suploc  7710  suprleubex  8712  nnsub  8759  supinfneg  9390  infsupneg  9391  ublbneg  9405  exbtwnzlemex  10027  uzsinds  10215  iseqovex  10229  seq3val  10231  seqvalcd  10232  seqf  10234  seqovcd  10236  monoord2  10250  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  seq3f1olemqsum  10273  seq3f1olemp  10275  seq3f1oleml  10276  seq3f1o  10277  bccl  10513  seq3shft  10610  caucvgre  10753  cvg1nlemcau  10756  resqrexlemglsq  10794  resqrexlemsqa  10796  resqrexlemex  10797  cau3lem  10886  zsumdc  11153  fsum3  11156  isumz  11158  isumss2  11162  fsumsersdc  11164  fsum3ser  11166  fisum0diag2  11216  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratz  11301  mertenslem2  11305  mertensabs  11306  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemzz  11690  bezoutlemeu  11695  bezoutlemle  11696  dfgcd3  11698  prmind2  11801  sqrt2irr  11840  hashdvds  11897  ennnfoneleminc  11924  ennnfonelemex  11927  ennnfonelemr  11936  ctinfom  11941  ctinf  11943  ctiunctlemudc  11950  tgcn  12377  mulcncflem  12759  suplociccreex  12771  dedekindicc  12780  nnsf  13199  nninfsellemqall  13211  nninfomni  13215