Theorem cbvralv 2726

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477

This theorem is referenced by:  cbvral2v  2739  cbvral3v  2741  reu7  2956  reusv3i  4491  omsinds  4655  cnvpom  5209  f1mpt  5815  tfrlem1  6363  tfrlemiubacc  6385  tfrlemi1  6387  tfr1onlemubacc  6401  tfr1onlemaccex  6403  tfrcllembxssdm  6411  tfrcllemubacc  6414  tfrcllemaccex  6416  tfrcllemres  6417  tfrcldm  6418  rdgon  6441  frecfcllem  6459  frecsuclem  6461  nneneq  6915  fimax2gtrilemstep  6958  supubti  7060  suplubti  7061  finomni  7201  nninfwlporlemd  7233  acfun  7269  exmidontriimlem3  7285  exmidontriimlem4  7286  exmidontriim  7287  ccfunen  7326  cc2  7329  cauappcvgprlemladdrl  7719  caucvgprlemcl  7738  caucvgprlemladdrl  7740  caucvgsrlembound  7856  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  suplocsrlem  7870  peano5nnnn  7954  axcaucvglemres  7961  axpre-suploc  7964  suprleubex  8975  nnsub  9023  supinfneg  9663  infsupneg  9664  infregelbex  9666  ublbneg  9681  exbtwnzlemex  10321  uzsinds  10518  iseqovex  10532  seq3val  10534  seqvalcd  10535  seqf  10538  seqovcd  10541  monoord2  10560  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  seq3f1olemqsum  10587  seq3f1olemp  10589  seq3f1oleml  10590  seq3f1o  10591  nn0ltexp2  10783  bccl  10841  seq3shft  10985  caucvgre  11128  cvg1nlemcau  11131  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  cau3lem  11261  zsumdc  11530  fsum3  11533  isumz  11535  isumss2  11539  fsumsersdc  11541  fsum3ser  11543  fisum0diag2  11593  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratz  11678  mertenslem2  11682  mertensabs  11683  zproddc  11725  fprodseq  11729  prod1dc  11732  fprodsplitdc  11742  zsupssdc  12094  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemzz  12142  bezoutlemeu  12147  bezoutlemle  12148  dfgcd3  12150  prmind2  12261  sqrt2irr  12303  hashdvds  12362  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemr  12583  ctinfom  12588  ctinf  12590  ctiunctlemudc  12597  ssnnctlemct  12606  nninfdclemp1  12610  tgcn  14387  mulcncflem  14786  suplociccreex  14803  dedekindicc  14812  nnsf  15565  nninfsellemqall  15575  nninfomni  15579  trirec0  15604  apdiff  15608  iswomni0  15611  dceqnconst  15620  dcapnconst  15621  neap0mkv  15629  ltlenmkv  15630