Theorem cbvralv 2704

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

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

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  cbvral2v  2717  cbvral3v  2719  reu7  2933  reusv3i  4460  omsinds  4622  cnvpom  5172  f1mpt  5772  tfrlem1  6309  tfrlemiubacc  6331  tfrlemi1  6333  tfr1onlemubacc  6347  tfr1onlemaccex  6349  tfrcllembxssdm  6357  tfrcllemubacc  6360  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  rdgon  6387  frecfcllem  6405  frecsuclem  6407  nneneq  6857  fimax2gtrilemstep  6900  supubti  6998  suplubti  6999  finomni  7138  nninfwlporlemd  7170  acfun  7206  exmidontriimlem3  7222  exmidontriimlem4  7223  exmidontriim  7224  ccfunen  7263  cc2  7266  cauappcvgprlemladdrl  7656  caucvgprlemcl  7675  caucvgprlemladdrl  7677  caucvgsrlembound  7793  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  suplocsrlem  7807  peano5nnnn  7891  axcaucvglemres  7898  axpre-suploc  7901  suprleubex  8911  nnsub  8958  supinfneg  9595  infsupneg  9596  infregelbex  9598  ublbneg  9613  exbtwnzlemex  10250  uzsinds  10442  iseqovex  10456  seq3val  10458  seqvalcd  10459  seqf  10461  seqovcd  10463  monoord2  10477  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  seq3f1olemqsum  10500  seq3f1olemp  10502  seq3f1oleml  10503  seq3f1o  10504  nn0ltexp2  10689  bccl  10747  seq3shft  10847  caucvgre  10990  cvg1nlemcau  10993  resqrexlemglsq  11031  resqrexlemsqa  11033  resqrexlemex  11034  cau3lem  11123  zsumdc  11392  fsum3  11395  isumz  11397  isumss2  11401  fsumsersdc  11403  fsum3ser  11405  fisum0diag2  11455  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratz  11540  mertenslem2  11544  mertensabs  11545  zproddc  11587  fprodseq  11591  prod1dc  11594  fprodsplitdc  11604  zsupssdc  11955  bezoutlemmain  11999  bezoutlemex  12002  bezoutlemzz  12003  bezoutlemeu  12008  bezoutlemle  12009  dfgcd3  12011  prmind2  12120  sqrt2irr  12162  hashdvds  12221  ennnfoneleminc  12412  ennnfonelemex  12415  ennnfonelemr  12424  ctinfom  12429  ctinf  12431  ctiunctlemudc  12438  ssnnctlemct  12447  nninfdclemcl  12449  nninfdclemp1  12451  tgcn  13711  mulcncflem  14093  suplociccreex  14105  dedekindicc  14114  nnsf  14757  nninfsellemqall  14767  nninfomni  14771  trirec0  14795  apdiff  14799  iswomni0  14802  dceqnconst  14810  dcapnconst  14811  neap0mkv  14819  ltlenmkv  14820