Theorem cbvralv 2696

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 1521	. 2 |- F/ y ph
2		nfv 1521	. 2 |- F/ x ps
3		cbvralv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvral 2692	1 |- ( A. x e. A ph <-> A. y e. A ps )

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

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453

This theorem is referenced by:  cbvral2v  2709  cbvral3v  2711  reu7  2925  reusv3i  4444  omsinds  4606  cnvpom  5153  f1mpt  5750  tfrlem1  6287  tfrlemiubacc  6309  tfrlemi1  6311  tfr1onlemubacc  6325  tfr1onlemaccex  6327  tfrcllembxssdm  6335  tfrcllemubacc  6338  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  rdgon  6365  frecfcllem  6383  frecsuclem  6385  nneneq  6835  fimax2gtrilemstep  6878  supubti  6976  suplubti  6977  finomni  7116  nninfwlporlemd  7148  acfun  7184  exmidontriimlem3  7200  exmidontriimlem4  7201  exmidontriim  7202  ccfunen  7226  cc2  7229  cauappcvgprlemladdrl  7619  caucvgprlemcl  7638  caucvgprlemladdrl  7640  caucvgsrlembound  7756  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  suplocsrlem  7770  peano5nnnn  7854  axcaucvglemres  7861  axpre-suploc  7864  suprleubex  8870  nnsub  8917  supinfneg  9554  infsupneg  9555  infregelbex  9557  ublbneg  9572  exbtwnzlemex  10206  uzsinds  10398  iseqovex  10412  seq3val  10414  seqvalcd  10415  seqf  10417  seqovcd  10419  monoord2  10433  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  seq3f1olemqsum  10456  seq3f1olemp  10458  seq3f1oleml  10459  seq3f1o  10460  nn0ltexp2  10644  bccl  10701  seq3shft  10802  caucvgre  10945  cvg1nlemcau  10948  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  cau3lem  11078  zsumdc  11347  fsum3  11350  isumz  11352  isumss2  11356  fsumsersdc  11358  fsum3ser  11360  fisum0diag2  11410  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratz  11495  mertenslem2  11499  mertensabs  11500  zproddc  11542  fprodseq  11546  prod1dc  11549  fprodsplitdc  11559  zsupssdc  11909  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemzz  11957  bezoutlemeu  11962  bezoutlemle  11963  dfgcd3  11965  prmind2  12074  sqrt2irr  12116  hashdvds  12175  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemr  12378  ctinfom  12383  ctinf  12385  ctiunctlemudc  12392  ssnnctlemct  12401  nninfdclemcl  12403  nninfdclemp1  12405  tgcn  13002  mulcncflem  13384  suplociccreex  13396  dedekindicc  13405  nnsf  14038  nninfsellemqall  14048  nninfomni  14052  trirec0  14076  apdiff  14080  iswomni0  14083  dceqnconst  14091  dcapnconst  14092