Theorem cbvralv 2626

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393

This theorem is referenced by:  cbvral2v  2634  cbvral3v  2636  reu7  2846  reusv3i  4338  omsinds  4493  cnvpom  5037  f1mpt  5624  grprinvlem  5917  grprinvd  5918  tfrlem1  6157  tfrlemiubacc  6179  tfrlemi1  6181  tfr1onlemubacc  6195  tfr1onlemaccex  6197  tfrcllembxssdm  6205  tfrcllemubacc  6208  tfrcllemaccex  6210  tfrcllemres  6211  tfrcldm  6212  rdgon  6235  frecfcllem  6253  frecsuclem  6255  nneneq  6702  fimax2gtrilemstep  6745  supubti  6836  suplubti  6837  finomni  6960  acfun  7008  cauappcvgprlemladdrl  7407  caucvgprlemcl  7426  caucvgprlemladdrl  7428  caucvgsrlembound  7530  caucvgsrlemgt1  7531  caucvgsrlemoffres  7536  peano5nnnn  7621  axcaucvglemres  7628  suprleubex  8616  nnsub  8663  supinfneg  9286  infsupneg  9287  ublbneg  9301  exbtwnzlemex  9914  uzsinds  10102  iseqovex  10116  seq3val  10118  seqvalcd  10119  seqf  10121  seqovcd  10123  monoord2  10137  iseqf1olemjpcl  10155  iseqf1olemqpcl  10156  seq3f1olemqsum  10160  seq3f1olemp  10162  seq3f1oleml  10163  seq3f1o  10164  bccl  10400  seq3shft  10497  caucvgre  10639  cvg1nlemcau  10642  resqrexlemglsq  10680  resqrexlemsqa  10682  resqrexlemex  10683  cau3lem  10772  zsumdc  11039  fsum3  11042  isumz  11044  isumss2  11048  fsumsersdc  11050  fsum3ser  11052  fisum0diag2  11102  cvgratnnlemnexp  11179  cvgratnnlemmn  11180  cvgratz  11187  mertenslem2  11191  mertensabs  11192  bezoutlemmain  11526  bezoutlemex  11529  bezoutlemzz  11530  bezoutlemeu  11535  bezoutlemle  11536  dfgcd3  11538  prmind2  11641  sqrt2irr  11680  hashdvds  11736  ennnfoneleminc  11763  ennnfonelemex  11766  ennnfonelemr  11775  ctinfom  11780  ctinf  11782  ctiunctlemudc  11787  tgcn  12213  mulcncflem  12570  nnsf  12880  nninfsellemqall  12892  nninfomni  12896