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  9286  nnsub  9345  supinfneg  10004  infsupneg  10005  infregelbex  10007  ublbneg  10022  irraddap  10056  zsupssdc  10683  exbtwnzlemex  10694  uzsinds  10894  iseqovex  10908  seq3val  10910  seqvalcd  10911  seqf  10914  seqovcd  10917  monoord2  10936  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seq3f1olemqsum  10963  seq3f1olemp  10965  seq3f1oleml  10966  seq3f1o  10967  nn0ltexp2  11161  bccl  11219  seq3shft  11617  caucvgre  11761  cvg1nlemcau  11764  resqrexlemglsq  11802  resqrexlemsqa  11804  resqrexlemex  11805  cau3lem  11895  zsumdc  12167  fsum3  12170  isumz  12172  isumss2  12176  fsumsersdc  12178  fsum3ser  12180  fisum0diag2  12230  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratz  12315  mertenslem2  12319  mertensabs  12320  zproddc  12362  fprodseq  12366  prod1dc  12369  fprodsplitdc  12379  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemzz  12795  bezoutlemeu  12800  bezoutlemle  12801  dfgcd3  12803  prmind2  12914  sqrt2irr  12957  hashdvds  13019  ballotfilemefi  13286  ballotfilemodife  13289  ennnfoneleminc  13351  ennnfonelemex  13354  ennnfonelemr  13363  ctinfom  13368  ctinf  13370  ctiunctlemudc  13377  ssnnctlemct  13386  nninfdclemp1  13390  mplsubgfilemcl  15139  tgcn  15358  mulcncflem  15757  suplociccreex  15774  dedekindicc  15783  vtxedgfi  16628  vtxlpfi  16629  nnsf  17146  nninfsellemqall  17156  nninfomni  17160  repiecef  17175  trirec0  17191  apdiff  17195  iswomni0  17199  dceqnconst  17208  dcapnconst  17209  neap0mkv  17217  ltlenmkv  17218