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  4607  omsinds  4771  cnvpom  5333  f1mpt  5980  tfrlem1  6583  tfrlemiubacc  6605  tfrlemi1  6607  tfr1onlemubacc  6621  tfr1onlemaccex  6623  tfrcllembxssdm  6631  tfrcllemubacc  6634  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  rdgon  6661  frecfcllem  6679  frecsuclem  6681  nneneq  7162  fimax2gtrilemstep  7209  supubti  7345  suplubti  7346  finomni  7486  nninfwlporlemd  7518  nninfinfwlpo  7526  acfun  7569  exmidontriimlem3  7585  exmidontriimlem4  7586  exmidontriim  7587  ccfunen  7636  cc2  7639  cauappcvgprlemladdrl  8030  caucvgprlemcl  8049  caucvgprlemladdrl  8051  caucvgsrlembound  8167  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  suplocsrlem  8181  peano5nnnn  8265  axcaucvglemres  8272  axpre-suploc  8275  suprleubex  9292  nnsub  9352  supinfneg  10011  infsupneg  10012  infregelbex  10014  ublbneg  10029  irraddap  10063  zsupssdc  10690  exbtwnzlemex  10701  uzsinds  10902  iseqovex  10916  seq3val  10918  seqvalcd  10919  seqf  10922  seqovcd  10925  monoord2  10944  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  seq3f1olemqsum  10971  seq3f1olemp  10973  seq3f1oleml  10974  seq3f1o  10975  nn0ltexp2  11169  bccl  11227  seq3shft  11625  caucvgre  11769  cvg1nlemcau  11772  resqrexlemglsq  11810  resqrexlemsqa  11812  resqrexlemex  11813  cau3lem  11903  zsumdc  12176  fsum3  12179  isumz  12181  isumss2  12185  fsumsersdc  12187  fsum3ser  12189  fisum0diag2  12239  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratz  12324  mertenslem2  12328  mertensabs  12329  zproddc  12371  fprodseq  12375  prod1dc  12378  fprodsplitdc  12388  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemzz  12804  bezoutlemeu  12809  bezoutlemle  12810  dfgcd3  12812  prmind2  12923  sqrt2irr  12966  hashdvds  13028  ballotfilemefi  13295  ballotfilemodife  13298  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemr  13372  ctinfom  13377  ctinf  13379  ctiunctlemudc  13386  ssnnctlemct  13395  nninfdclemp1  13399  psrbaglefifi  15172  mplsubgfilemcl  15215  tgcn  15434  mulcncflem  15833  suplociccreex  15850  dedekindicc  15859  vtxedgfi  16735  vtxlpfi  16736  nnsf  17254  nninfsellemqall  17264  nninfomni  17268  repiecef  17283  trirec0  17300  apdiff  17304  iswomni0  17308  dceqnconst  17317  dcapnconst  17318  neap0mkv  17326  ltlenmkv  17327