Theorem cbvralv 2705

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

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

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  cbvral2v  2718  cbvral3v  2720  reu7  2934  reusv3i  4461  omsinds  4623  cnvpom  5173  f1mpt  5774  tfrlem1  6311  tfrlemiubacc  6333  tfrlemi1  6335  tfr1onlemubacc  6349  tfr1onlemaccex  6351  tfrcllembxssdm  6359  tfrcllemubacc  6362  tfrcllemaccex  6364  tfrcllemres  6365  tfrcldm  6366  rdgon  6389  frecfcllem  6407  frecsuclem  6409  nneneq  6859  fimax2gtrilemstep  6902  supubti  7000  suplubti  7001  finomni  7140  nninfwlporlemd  7172  acfun  7208  exmidontriimlem3  7224  exmidontriimlem4  7225  exmidontriim  7226  ccfunen  7265  cc2  7268  cauappcvgprlemladdrl  7658  caucvgprlemcl  7677  caucvgprlemladdrl  7679  caucvgsrlembound  7795  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  suplocsrlem  7809  peano5nnnn  7893  axcaucvglemres  7900  axpre-suploc  7903  suprleubex  8913  nnsub  8960  supinfneg  9597  infsupneg  9598  infregelbex  9600  ublbneg  9615  exbtwnzlemex  10252  uzsinds  10444  iseqovex  10458  seq3val  10460  seqvalcd  10461  seqf  10463  seqovcd  10465  monoord2  10479  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  seq3f1olemqsum  10502  seq3f1olemp  10504  seq3f1oleml  10505  seq3f1o  10506  nn0ltexp2  10691  bccl  10749  seq3shft  10849  caucvgre  10992  cvg1nlemcau  10995  resqrexlemglsq  11033  resqrexlemsqa  11035  resqrexlemex  11036  cau3lem  11125  zsumdc  11394  fsum3  11397  isumz  11399  isumss2  11403  fsumsersdc  11405  fsum3ser  11407  fisum0diag2  11457  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratz  11542  mertenslem2  11546  mertensabs  11547  zproddc  11589  fprodseq  11593  prod1dc  11596  fprodsplitdc  11606  zsupssdc  11957  bezoutlemmain  12001  bezoutlemex  12004  bezoutlemzz  12005  bezoutlemeu  12010  bezoutlemle  12011  dfgcd3  12013  prmind2  12122  sqrt2irr  12164  hashdvds  12223  ennnfoneleminc  12414  ennnfonelemex  12417  ennnfonelemr  12426  ctinfom  12431  ctinf  12433  ctiunctlemudc  12440  ssnnctlemct  12449  nninfdclemcl  12451  nninfdclemp1  12453  tgcn  13793  mulcncflem  14175  suplociccreex  14187  dedekindicc  14196  nnsf  14839  nninfsellemqall  14849  nninfomni  14853  trirec0  14877  apdiff  14881  iswomni0  14884  dceqnconst  14893  dcapnconst  14894  neap0mkv  14902  ltlenmkv  14903