Theorem cbvralv 2786

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  cbvral2v  2799  cbvral3v  2801  reu7  3021  reusv3i  4605  omsinds  4769  cnvpom  5330  f1mpt  5977  tfrlem1  6579  tfrlemiubacc  6601  tfrlemi1  6603  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfrcllembxssdm  6627  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  rdgon  6657  frecfcllem  6675  frecsuclem  6677  nneneq  7158  fimax2gtrilemstep  7205  supubti  7339  suplubti  7340  finomni  7480  nninfwlporlemd  7512  nninfinfwlpo  7520  acfun  7563  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  ccfunen  7630  cc2  7633  cauappcvgprlemladdrl  8024  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgsrlembound  8161  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  suplocsrlem  8175  peano5nnnn  8259  axcaucvglemres  8266  axpre-suploc  8269  suprleubex  9284  nnsub  9343  supinfneg  9995  infsupneg  9996  infregelbex  9998  ublbneg  10013  zsupssdc  10673  exbtwnzlemex  10684  uzsinds  10881  iseqovex  10895  seq3val  10897  seqvalcd  10898  seqf  10901  seqovcd  10904  monoord2  10923  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  seq3f1olemqsum  10950  seq3f1olemp  10952  seq3f1oleml  10953  seq3f1o  10954  nn0ltexp2  11147  bccl  11205  seq3shft  11603  caucvgre  11747  cvg1nlemcau  11750  resqrexlemglsq  11788  resqrexlemsqa  11790  resqrexlemex  11791  cau3lem  11880  zsumdc  12151  fsum3  12154  isumz  12156  isumss2  12160  fsumsersdc  12162  fsum3ser  12164  fisum0diag2  12214  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratz  12299  mertenslem2  12303  mertensabs  12304  zproddc  12346  fprodseq  12350  prod1dc  12353  fprodsplitdc  12363  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemzz  12779  bezoutlemeu  12784  bezoutlemle  12785  dfgcd3  12787  prmind2  12898  sqrt2irr  12940  hashdvds  12999  ballotfilemefi  13237  ballotfilemodife  13240  ennnfoneleminc  13302  ennnfonelemex  13305  ennnfonelemr  13314  ctinfom  13319  ctinf  13321  ctiunctlemudc  13328  ssnnctlemct  13337  nninfdclemp1  13341  mplsubgfilemcl  15090  tgcn  15309  mulcncflem  15708  suplociccreex  15725  dedekindicc  15734  vtxedgfi  16530  vtxlpfi  16531  nnsf  17048  nninfsellemqall  17058  nninfomni  17062  repiecef  17077  trirec0  17093  apdiff  17097  iswomni0  17101  dceqnconst  17110  dcapnconst  17111  neap0mkv  17119  ltlenmkv  17120