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  4550  omsinds  4714  cnvpom  5271  f1mpt  5901  tfrlem1  6460  tfrlemiubacc  6482  tfrlemi1  6484  tfr1onlemubacc  6498  tfr1onlemaccex  6500  tfrcllembxssdm  6508  tfrcllemubacc  6511  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  rdgon  6538  frecfcllem  6556  frecsuclem  6558  nneneq  7026  fimax2gtrilemstep  7071  supubti  7177  suplubti  7178  finomni  7318  nninfwlporlemd  7350  nninfinfwlpo  7358  acfun  7400  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  ccfunen  7461  cc2  7464  cauappcvgprlemladdrl  7855  caucvgprlemcl  7874  caucvgprlemladdrl  7876  caucvgsrlembound  7992  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  suplocsrlem  8006  peano5nnnn  8090  axcaucvglemres  8097  axpre-suploc  8100  suprleubex  9112  nnsub  9160  supinfneg  9802  infsupneg  9803  infregelbex  9805  ublbneg  9820  zsupssdc  10470  exbtwnzlemex  10481  uzsinds  10678  iseqovex  10692  seq3val  10694  seqvalcd  10695  seqf  10698  seqovcd  10701  monoord2  10720  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seq3f1olemqsum  10747  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  nn0ltexp2  10943  bccl  11001  seq3shft  11365  caucvgre  11508  cvg1nlemcau  11511  resqrexlemglsq  11549  resqrexlemsqa  11551  resqrexlemex  11552  cau3lem  11641  zsumdc  11911  fsum3  11914  isumz  11916  isumss2  11920  fsumsersdc  11922  fsum3ser  11924  fisum0diag2  11974  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratz  12059  mertenslem2  12063  mertensabs  12064  zproddc  12106  fprodseq  12110  prod1dc  12113  fprodsplitdc  12123  bezoutlemmain  12535  bezoutlemex  12538  bezoutlemzz  12539  bezoutlemeu  12544  bezoutlemle  12545  dfgcd3  12547  prmind2  12658  sqrt2irr  12700  hashdvds  12759  ennnfoneleminc  12998  ennnfonelemex  13001  ennnfonelemr  13010  ctinfom  13015  ctinf  13017  ctiunctlemudc  13024  ssnnctlemct  13033  nninfdclemp1  13037  mplsubgfilemcl  14679  tgcn  14898  mulcncflem  15297  suplociccreex  15314  dedekindicc  15323  vtxedgfi  16049  vtxlpfi  16050  nnsf  16459  nninfsellemqall  16469  nninfomni  16473  trirec0  16500  apdiff  16504  iswomni0  16507  dceqnconst  16516  dcapnconst  16517  neap0mkv  16525  ltlenmkv  16526