Theorem cbvralv 2654

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 2650	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

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

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421

This theorem is referenced by:  cbvralvw  2658  cbvral2v  2665  cbvral3v  2667  reu7  2879  reusv3i  4380  omsinds  4535  cnvpom  5081  f1mpt  5672  grprinvlem  5965  grprinvd  5966  tfrlem1  6205  tfrlemiubacc  6227  tfrlemi1  6229  tfr1onlemubacc  6243  tfr1onlemaccex  6245  tfrcllembxssdm  6253  tfrcllemubacc  6256  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  rdgon  6283  frecfcllem  6301  frecsuclem  6303  nneneq  6751  fimax2gtrilemstep  6794  supubti  6886  suplubti  6887  finomni  7012  acfun  7063  ccfunen  7079  cc2  7082  cauappcvgprlemladdrl  7468  caucvgprlemcl  7487  caucvgprlemladdrl  7489  caucvgsrlembound  7605  caucvgsrlemgt1  7606  caucvgsrlemoffres  7611  suplocsrlem  7619  peano5nnnn  7703  axcaucvglemres  7710  axpre-suploc  7713  suprleubex  8715  nnsub  8762  supinfneg  9393  infsupneg  9394  ublbneg  9408  exbtwnzlemex  10030  uzsinds  10218  iseqovex  10232  seq3val  10234  seqvalcd  10235  seqf  10237  seqovcd  10239  monoord2  10253  iseqf1olemjpcl  10271  iseqf1olemqpcl  10272  seq3f1olemqsum  10276  seq3f1olemp  10278  seq3f1oleml  10279  seq3f1o  10280  bccl  10516  seq3shft  10613  caucvgre  10756  cvg1nlemcau  10759  resqrexlemglsq  10797  resqrexlemsqa  10799  resqrexlemex  10800  cau3lem  10889  zsumdc  11156  fsum3  11159  isumz  11161  isumss2  11165  fsumsersdc  11167  fsum3ser  11169  fisum0diag2  11219  cvgratnnlemnexp  11296  cvgratnnlemmn  11297  cvgratz  11304  mertenslem2  11308  mertensabs  11309  bezoutlemmain  11689  bezoutlemex  11692  bezoutlemzz  11693  bezoutlemeu  11698  bezoutlemle  11699  dfgcd3  11701  prmind2  11804  sqrt2irr  11843  hashdvds  11900  ennnfoneleminc  11927  ennnfonelemex  11930  ennnfonelemr  11939  ctinfom  11944  ctinf  11946  ctiunctlemudc  11953  tgcn  12380  mulcncflem  12762  suplociccreex  12774  dedekindicc  12783  nnsf  13202  nninfsellemqall  13214  nninfomni  13218