Theorem cbvralv 2680

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)

Hypothesis

Ref	Expression
cbvralv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvralv	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralv

Step	Hyp	Ref	Expression
1		nfv 1508	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1508	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 2676	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440

This theorem is referenced by:  cbvral2v  2691  cbvral3v  2693  reu7  2907  reusv3i  4419  omsinds  4581  cnvpom  5128  f1mpt  5721  grprinvlem  6015  grprinvd  6016  tfrlem1  6255  tfrlemiubacc  6277  tfrlemi1  6279  tfr1onlemubacc  6293  tfr1onlemaccex  6295  tfrcllembxssdm  6303  tfrcllemubacc  6306  tfrcllemaccex  6308  tfrcllemres  6309  tfrcldm  6310  rdgon  6333  frecfcllem  6351  frecsuclem  6353  nneneq  6802  fimax2gtrilemstep  6845  supubti  6943  suplubti  6944  finomni  7083  acfun  7142  exmidontriimlem3  7158  exmidontriimlem4  7159  exmidontriim  7160  ccfunen  7184  cc2  7187  cauappcvgprlemladdrl  7577  caucvgprlemcl  7596  caucvgprlemladdrl  7598  caucvgsrlembound  7714  caucvgsrlemgt1  7715  caucvgsrlemoffres  7720  suplocsrlem  7728  peano5nnnn  7812  axcaucvglemres  7819  axpre-suploc  7822  suprleubex  8825  nnsub  8872  supinfneg  9506  infsupneg  9507  infregelbex  9509  ublbneg  9522  exbtwnzlemex  10149  uzsinds  10341  iseqovex  10355  seq3val  10357  seqvalcd  10358  seqf  10360  seqovcd  10362  monoord2  10376  iseqf1olemjpcl  10394  iseqf1olemqpcl  10395  seq3f1olemqsum  10399  seq3f1olemp  10401  seq3f1oleml  10402  seq3f1o  10403  bccl  10641  seq3shft  10738  caucvgre  10881  cvg1nlemcau  10884  resqrexlemglsq  10922  resqrexlemsqa  10924  resqrexlemex  10925  cau3lem  11014  zsumdc  11281  fsum3  11284  isumz  11286  isumss2  11290  fsumsersdc  11292  fsum3ser  11294  fisum0diag2  11344  cvgratnnlemnexp  11421  cvgratnnlemmn  11422  cvgratz  11429  mertenslem2  11433  mertensabs  11434  zproddc  11476  fprodseq  11480  prod1dc  11483  fprodsplitdc  11493  bezoutlemmain  11882  bezoutlemex  11885  bezoutlemzz  11886  bezoutlemeu  11891  bezoutlemle  11892  dfgcd3  11894  prmind2  11997  sqrt2irr  12037  hashdvds  12096  ennnfoneleminc  12151  ennnfonelemex  12154  ennnfonelemr  12163  ctinfom  12168  ctinf  12170  ctiunctlemudc  12177  ssnnctlemct  12186  nninfdclemcl  12190  nninfdclemp1  12192  tgcn  12619  mulcncflem  13001  suplociccreex  13013  dedekindicc  13022  nnsf  13588  nninfsellemqall  13598  nninfomni  13602  trirec0  13626  apdiff  13630  iswomni0  13633  dceqnconst  13641  dcapnconst  13642