Theorem cbvralv 2765

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

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

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  cbvral2v  2778  cbvral3v  2780  reu7  2998  reusv3i  4551  omsinds  4715  cnvpom  5274  f1mpt  5904  tfrlem1  6465  tfrlemiubacc  6487  tfrlemi1  6489  tfr1onlemubacc  6503  tfr1onlemaccex  6505  tfrcllembxssdm  6513  tfrcllemubacc  6516  tfrcllemaccex  6518  tfrcllemres  6519  tfrcldm  6520  rdgon  6543  frecfcllem  6561  frecsuclem  6563  nneneq  7031  fimax2gtrilemstep  7076  supubti  7182  suplubti  7183  finomni  7323  nninfwlporlemd  7355  nninfinfwlpo  7363  acfun  7405  exmidontriimlem3  7421  exmidontriimlem4  7422  exmidontriim  7423  ccfunen  7466  cc2  7469  cauappcvgprlemladdrl  7860  caucvgprlemcl  7879  caucvgprlemladdrl  7881  caucvgsrlembound  7997  caucvgsrlemgt1  7998  caucvgsrlemoffres  8003  suplocsrlem  8011  peano5nnnn  8095  axcaucvglemres  8102  axpre-suploc  8105  suprleubex  9117  nnsub  9165  supinfneg  9807  infsupneg  9808  infregelbex  9810  ublbneg  9825  zsupssdc  10475  exbtwnzlemex  10486  uzsinds  10683  iseqovex  10697  seq3val  10699  seqvalcd  10700  seqf  10703  seqovcd  10706  monoord2  10725  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  seq3f1olemqsum  10752  seq3f1olemp  10754  seq3f1oleml  10755  seq3f1o  10756  nn0ltexp2  10948  bccl  11006  seq3shft  11370  caucvgre  11513  cvg1nlemcau  11516  resqrexlemglsq  11554  resqrexlemsqa  11556  resqrexlemex  11557  cau3lem  11646  zsumdc  11916  fsum3  11919  isumz  11921  isumss2  11925  fsumsersdc  11927  fsum3ser  11929  fisum0diag2  11979  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  cvgratz  12064  mertenslem2  12068  mertensabs  12069  zproddc  12111  fprodseq  12115  prod1dc  12118  fprodsplitdc  12128  bezoutlemmain  12540  bezoutlemex  12543  bezoutlemzz  12544  bezoutlemeu  12549  bezoutlemle  12550  dfgcd3  12552  prmind2  12663  sqrt2irr  12705  hashdvds  12764  ennnfoneleminc  13003  ennnfonelemex  13006  ennnfonelemr  13015  ctinfom  13020  ctinf  13022  ctiunctlemudc  13029  ssnnctlemct  13038  nninfdclemp1  13042  mplsubgfilemcl  14684  tgcn  14903  mulcncflem  15302  suplociccreex  15319  dedekindicc  15328  vtxedgfi  16075  vtxlpfi  16076  nnsf  16485  nninfsellemqall  16495  nninfomni  16499  trirec0  16526  apdiff  16530  iswomni0  16533  dceqnconst  16542  dcapnconst  16543  neap0mkv  16551  ltlenmkv  16552