Theorem cbvralv 2765

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

Syntax hints:   -> wi 4   <-> wb 105   A.wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  cbvral2v  2778  cbvral3v  2780  reu7  2998  reusv3i  4550  omsinds  4714  cnvpom  5271  f1mpt  5895  tfrlem1  6454  tfrlemiubacc  6476  tfrlemi1  6478  tfr1onlemubacc  6492  tfr1onlemaccex  6494  tfrcllembxssdm  6502  tfrcllemubacc  6505  tfrcllemaccex  6507  tfrcllemres  6508  tfrcldm  6509  rdgon  6532  frecfcllem  6550  frecsuclem  6552  nneneq  7018  fimax2gtrilemstep  7062  supubti  7166  suplubti  7167  finomni  7307  nninfwlporlemd  7339  nninfinfwlpo  7347  acfun  7389  exmidontriimlem3  7405  exmidontriimlem4  7406  exmidontriim  7407  ccfunen  7450  cc2  7453  cauappcvgprlemladdrl  7844  caucvgprlemcl  7863  caucvgprlemladdrl  7865  caucvgsrlembound  7981  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  suplocsrlem  7995  peano5nnnn  8079  axcaucvglemres  8086  axpre-suploc  8089  suprleubex  9101  nnsub  9149  supinfneg  9790  infsupneg  9791  infregelbex  9793  ublbneg  9808  zsupssdc  10458  exbtwnzlemex  10469  uzsinds  10666  iseqovex  10680  seq3val  10682  seqvalcd  10683  seqf  10686  seqovcd  10689  monoord2  10708  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  seq3f1olemqsum  10735  seq3f1olemp  10737  seq3f1oleml  10738  seq3f1o  10739  nn0ltexp2  10931  bccl  10989  seq3shft  11349  caucvgre  11492  cvg1nlemcau  11495  resqrexlemglsq  11533  resqrexlemsqa  11535  resqrexlemex  11536  cau3lem  11625  zsumdc  11895  fsum3  11898  isumz  11900  isumss2  11904  fsumsersdc  11906  fsum3ser  11908  fisum0diag2  11958  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratz  12043  mertenslem2  12047  mertensabs  12048  zproddc  12090  fprodseq  12094  prod1dc  12097  fprodsplitdc  12107  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemzz  12523  bezoutlemeu  12528  bezoutlemle  12529  dfgcd3  12531  prmind2  12642  sqrt2irr  12684  hashdvds  12743  ennnfoneleminc  12982  ennnfonelemex  12985  ennnfonelemr  12994  ctinfom  12999  ctinf  13001  ctiunctlemudc  13008  ssnnctlemct  13017  nninfdclemp1  13021  mplsubgfilemcl  14663  tgcn  14882  mulcncflem  15281  suplociccreex  15298  dedekindicc  15307  nnsf  16371  nninfsellemqall  16381  nninfomni  16385  trirec0  16412  apdiff  16416  iswomni0  16419  dceqnconst  16428  dcapnconst  16429  neap0mkv  16437  ltlenmkv  16438