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  7340  suplubti  7341  finomni  7481  nninfwlporlemd  7513  nninfinfwlpo  7521  acfun  7564  exmidontriimlem3  7580  exmidontriimlem4  7581  exmidontriim  7582  ccfunen  7631  cc2  7634  cauappcvgprlemladdrl  8025  caucvgprlemcl  8044  caucvgprlemladdrl  8046  caucvgsrlembound  8162  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  suplocsrlem  8176  peano5nnnn  8260  axcaucvglemres  8267  axpre-suploc  8270  suprleubex  9287  nnsub  9346  supinfneg  10005  infsupneg  10006  infregelbex  10008  ublbneg  10023  irraddap  10057  zsupssdc  10684  exbtwnzlemex  10695  uzsinds  10895  iseqovex  10909  seq3val  10911  seqvalcd  10912  seqf  10915  seqovcd  10918  monoord2  10937  iseqf1olemjpcl  10959  iseqf1olemqpcl  10960  seq3f1olemqsum  10964  seq3f1olemp  10966  seq3f1oleml  10967  seq3f1o  10968  nn0ltexp2  11162  bccl  11220  seq3shft  11618  caucvgre  11762  cvg1nlemcau  11765  resqrexlemglsq  11803  resqrexlemsqa  11805  resqrexlemex  11806  cau3lem  11896  zsumdc  12169  fsum3  12172  isumz  12174  isumss2  12178  fsumsersdc  12180  fsum3ser  12182  fisum0diag2  12232  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratz  12317  mertenslem2  12321  mertensabs  12322  zproddc  12364  fprodseq  12368  prod1dc  12371  fprodsplitdc  12381  bezoutlemmain  12793  bezoutlemex  12796  bezoutlemzz  12797  bezoutlemeu  12802  bezoutlemle  12803  dfgcd3  12805  prmind2  12916  sqrt2irr  12959  hashdvds  13021  ballotfilemefi  13288  ballotfilemodife  13291  ennnfoneleminc  13353  ennnfonelemex  13356  ennnfonelemr  13365  ctinfom  13370  ctinf  13372  ctiunctlemudc  13379  ssnnctlemct  13388  nninfdclemp1  13392  psrbaglefifi  15114  mplsubgfilemcl  15142  tgcn  15361  mulcncflem  15760  suplociccreex  15777  dedekindicc  15786  vtxedgfi  16652  vtxlpfi  16653  nnsf  17170  nninfsellemqall  17180  nninfomni  17184  repiecef  17199  trirec0  17215  apdiff  17219  iswomni0  17223  dceqnconst  17232  dcapnconst  17233  neap0mkv  17241  ltlenmkv  17242