Theorem cbvralv 2738

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

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

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489

This theorem is referenced by:  cbvral2v  2751  cbvral3v  2753  reu7  2968  reusv3i  4507  omsinds  4671  cnvpom  5226  f1mpt  5842  tfrlem1  6396  tfrlemiubacc  6418  tfrlemi1  6420  tfr1onlemubacc  6434  tfr1onlemaccex  6436  tfrcllembxssdm  6444  tfrcllemubacc  6447  tfrcllemaccex  6449  tfrcllemres  6450  tfrcldm  6451  rdgon  6474  frecfcllem  6492  frecsuclem  6494  nneneq  6956  fimax2gtrilemstep  6999  supubti  7103  suplubti  7104  finomni  7244  nninfwlporlemd  7276  nninfinfwlpo  7284  acfun  7321  exmidontriimlem3  7337  exmidontriimlem4  7338  exmidontriim  7339  ccfunen  7378  cc2  7381  cauappcvgprlemladdrl  7772  caucvgprlemcl  7791  caucvgprlemladdrl  7793  caucvgsrlembound  7909  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  suplocsrlem  7923  peano5nnnn  8007  axcaucvglemres  8014  axpre-suploc  8017  suprleubex  9029  nnsub  9077  supinfneg  9718  infsupneg  9719  infregelbex  9721  ublbneg  9736  zsupssdc  10383  exbtwnzlemex  10394  uzsinds  10591  iseqovex  10605  seq3val  10607  seqvalcd  10608  seqf  10611  seqovcd  10614  monoord2  10633  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  seq3f1olemqsum  10660  seq3f1olemp  10662  seq3f1oleml  10663  seq3f1o  10664  nn0ltexp2  10856  bccl  10914  seq3shft  11182  caucvgre  11325  cvg1nlemcau  11328  resqrexlemglsq  11366  resqrexlemsqa  11368  resqrexlemex  11369  cau3lem  11458  zsumdc  11728  fsum3  11731  isumz  11733  isumss2  11737  fsumsersdc  11739  fsum3ser  11741  fisum0diag2  11791  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratz  11876  mertenslem2  11880  mertensabs  11881  zproddc  11923  fprodseq  11927  prod1dc  11930  fprodsplitdc  11940  bezoutlemmain  12352  bezoutlemex  12355  bezoutlemzz  12356  bezoutlemeu  12361  bezoutlemle  12362  dfgcd3  12364  prmind2  12475  sqrt2irr  12517  hashdvds  12576  ennnfoneleminc  12815  ennnfonelemex  12818  ennnfonelemr  12827  ctinfom  12832  ctinf  12834  ctiunctlemudc  12841  ssnnctlemct  12850  nninfdclemp1  12854  mplsubgfilemcl  14494  tgcn  14713  mulcncflem  15112  suplociccreex  15129  dedekindicc  15138  nnsf  15979  nninfsellemqall  15989  nninfomni  15993  trirec0  16020  apdiff  16024  iswomni0  16027  dceqnconst  16036  dcapnconst  16037  neap0mkv  16045  ltlenmkv  16046