Theorem cbvralv 2742

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491

This theorem is referenced by:  cbvral2v  2755  cbvral3v  2757  reu7  2975  reusv3i  4524  omsinds  4688  cnvpom  5244  f1mpt  5863  tfrlem1  6417  tfrlemiubacc  6439  tfrlemi1  6441  tfr1onlemubacc  6455  tfr1onlemaccex  6457  tfrcllembxssdm  6465  tfrcllemubacc  6468  tfrcllemaccex  6470  tfrcllemres  6471  tfrcldm  6472  rdgon  6495  frecfcllem  6513  frecsuclem  6515  nneneq  6979  fimax2gtrilemstep  7023  supubti  7127  suplubti  7128  finomni  7268  nninfwlporlemd  7300  nninfinfwlpo  7308  acfun  7350  exmidontriimlem3  7366  exmidontriimlem4  7367  exmidontriim  7368  ccfunen  7411  cc2  7414  cauappcvgprlemladdrl  7805  caucvgprlemcl  7824  caucvgprlemladdrl  7826  caucvgsrlembound  7942  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  suplocsrlem  7956  peano5nnnn  8040  axcaucvglemres  8047  axpre-suploc  8050  suprleubex  9062  nnsub  9110  supinfneg  9751  infsupneg  9752  infregelbex  9754  ublbneg  9769  zsupssdc  10418  exbtwnzlemex  10429  uzsinds  10626  iseqovex  10640  seq3val  10642  seqvalcd  10643  seqf  10646  seqovcd  10649  monoord2  10668  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  seq3f1olemqsum  10695  seq3f1olemp  10697  seq3f1oleml  10698  seq3f1o  10699  nn0ltexp2  10891  bccl  10949  seq3shft  11264  caucvgre  11407  cvg1nlemcau  11410  resqrexlemglsq  11448  resqrexlemsqa  11450  resqrexlemex  11451  cau3lem  11540  zsumdc  11810  fsum3  11813  isumz  11815  isumss2  11819  fsumsersdc  11821  fsum3ser  11823  fisum0diag2  11873  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratz  11958  mertenslem2  11962  mertensabs  11963  zproddc  12005  fprodseq  12009  prod1dc  12012  fprodsplitdc  12022  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemzz  12438  bezoutlemeu  12443  bezoutlemle  12444  dfgcd3  12446  prmind2  12557  sqrt2irr  12599  hashdvds  12658  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemr  12909  ctinfom  12914  ctinf  12916  ctiunctlemudc  12923  ssnnctlemct  12932  nninfdclemp1  12936  mplsubgfilemcl  14576  tgcn  14795  mulcncflem  15194  suplociccreex  15211  dedekindicc  15220  nnsf  16144  nninfsellemqall  16154  nninfomni  16158  trirec0  16185  apdiff  16189  iswomni0  16192  dceqnconst  16201  dcapnconst  16202  neap0mkv  16210  ltlenmkv  16211