Theorem cbvralv 2768

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

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

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516

This theorem is referenced by:  cbvral2v  2781  cbvral3v  2783  reu7  3002  reusv3i  4562  omsinds  4726  cnvpom  5286  f1mpt  5922  tfrlem1  6517  tfrlemiubacc  6539  tfrlemi1  6541  tfr1onlemubacc  6555  tfr1onlemaccex  6557  tfrcllembxssdm  6565  tfrcllemubacc  6568  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  rdgon  6595  frecfcllem  6613  frecsuclem  6615  nneneq  7086  fimax2gtrilemstep  7133  supubti  7258  suplubti  7259  finomni  7399  nninfwlporlemd  7431  nninfinfwlpo  7439  acfun  7482  exmidontriimlem3  7498  exmidontriimlem4  7499  exmidontriim  7500  ccfunen  7543  cc2  7546  cauappcvgprlemladdrl  7937  caucvgprlemcl  7956  caucvgprlemladdrl  7958  caucvgsrlembound  8074  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  suplocsrlem  8088  peano5nnnn  8172  axcaucvglemres  8179  axpre-suploc  8182  suprleubex  9193  nnsub  9241  supinfneg  9890  infsupneg  9891  infregelbex  9893  ublbneg  9908  zsupssdc  10561  exbtwnzlemex  10572  uzsinds  10769  iseqovex  10783  seq3val  10785  seqvalcd  10786  seqf  10789  seqovcd  10792  monoord2  10811  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  seq3f1olemqsum  10838  seq3f1olemp  10840  seq3f1oleml  10841  seq3f1o  10842  nn0ltexp2  11034  bccl  11092  seq3shft  11478  caucvgre  11621  cvg1nlemcau  11624  resqrexlemglsq  11662  resqrexlemsqa  11664  resqrexlemex  11665  cau3lem  11754  zsumdc  12025  fsum3  12028  isumz  12030  isumss2  12034  fsumsersdc  12036  fsum3ser  12038  fisum0diag2  12088  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratz  12173  mertenslem2  12177  mertensabs  12178  zproddc  12220  fprodseq  12224  prod1dc  12227  fprodsplitdc  12237  bezoutlemmain  12649  bezoutlemex  12652  bezoutlemzz  12653  bezoutlemeu  12658  bezoutlemle  12659  dfgcd3  12661  prmind2  12772  sqrt2irr  12814  hashdvds  12873  ennnfoneleminc  13112  ennnfonelemex  13115  ennnfonelemr  13124  ctinfom  13129  ctinf  13131  ctiunctlemudc  13138  ssnnctlemct  13147  nninfdclemp1  13151  mplsubgfilemcl  14800  tgcn  15019  mulcncflem  15418  suplociccreex  15435  dedekindicc  15444  vtxedgfi  16230  vtxlpfi  16231  nnsf  16731  nninfsellemqall  16741  nninfomni  16745  repiecef  16760  trirec0  16776  apdiff  16780  iswomni0  16784  dceqnconst  16793  dcapnconst  16794  neap0mkv  16802  ltlenmkv  16803