Theorem cbvralv 2729

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

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

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480

This theorem is referenced by:  cbvral2v  2742  cbvral3v  2744  reu7  2959  reusv3i  4494  omsinds  4658  cnvpom  5212  f1mpt  5818  tfrlem1  6366  tfrlemiubacc  6388  tfrlemi1  6390  tfr1onlemubacc  6404  tfr1onlemaccex  6406  tfrcllembxssdm  6414  tfrcllemubacc  6417  tfrcllemaccex  6419  tfrcllemres  6420  tfrcldm  6421  rdgon  6444  frecfcllem  6462  frecsuclem  6464  nneneq  6918  fimax2gtrilemstep  6961  supubti  7065  suplubti  7066  finomni  7206  nninfwlporlemd  7238  acfun  7274  exmidontriimlem3  7290  exmidontriimlem4  7291  exmidontriim  7292  ccfunen  7331  cc2  7334  cauappcvgprlemladdrl  7724  caucvgprlemcl  7743  caucvgprlemladdrl  7745  caucvgsrlembound  7861  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  suplocsrlem  7875  peano5nnnn  7959  axcaucvglemres  7966  axpre-suploc  7969  suprleubex  8981  nnsub  9029  supinfneg  9669  infsupneg  9670  infregelbex  9672  ublbneg  9687  zsupssdc  10328  exbtwnzlemex  10339  uzsinds  10536  iseqovex  10550  seq3val  10552  seqvalcd  10553  seqf  10556  seqovcd  10559  monoord2  10578  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  seq3f1olemqsum  10605  seq3f1olemp  10607  seq3f1oleml  10608  seq3f1o  10609  nn0ltexp2  10801  bccl  10859  seq3shft  11003  caucvgre  11146  cvg1nlemcau  11149  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  cau3lem  11279  zsumdc  11549  fsum3  11552  isumz  11554  isumss2  11558  fsumsersdc  11560  fsum3ser  11562  fisum0diag2  11612  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratz  11697  mertenslem2  11701  mertensabs  11702  zproddc  11744  fprodseq  11748  prod1dc  11751  fprodsplitdc  11761  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemzz  12169  bezoutlemeu  12174  bezoutlemle  12175  dfgcd3  12177  prmind2  12288  sqrt2irr  12330  hashdvds  12389  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemr  12640  ctinfom  12645  ctinf  12647  ctiunctlemudc  12654  ssnnctlemct  12663  nninfdclemp1  12667  tgcn  14444  mulcncflem  14843  suplociccreex  14860  dedekindicc  14869  nnsf  15649  nninfsellemqall  15659  nninfomni  15663  trirec0  15688  apdiff  15692  iswomni0  15695  dceqnconst  15704  dcapnconst  15705  neap0mkv  15713  ltlenmkv  15714