Theorem cbvralv 2729

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 1542	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1542	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 2725	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480

This theorem is referenced by:  cbvral2v  2742  cbvral3v  2744  reu7  2959  reusv3i  4495  omsinds  4659  cnvpom  5213  f1mpt  5821  tfrlem1  6375  tfrlemiubacc  6397  tfrlemi1  6399  tfr1onlemubacc  6413  tfr1onlemaccex  6415  tfrcllembxssdm  6423  tfrcllemubacc  6426  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  rdgon  6453  frecfcllem  6471  frecsuclem  6473  nneneq  6927  fimax2gtrilemstep  6970  supubti  7074  suplubti  7075  finomni  7215  nninfwlporlemd  7247  acfun  7290  exmidontriimlem3  7306  exmidontriimlem4  7307  exmidontriim  7308  ccfunen  7347  cc2  7350  cauappcvgprlemladdrl  7741  caucvgprlemcl  7760  caucvgprlemladdrl  7762  caucvgsrlembound  7878  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  suplocsrlem  7892  peano5nnnn  7976  axcaucvglemres  7983  axpre-suploc  7986  suprleubex  8998  nnsub  9046  supinfneg  9686  infsupneg  9687  infregelbex  9689  ublbneg  9704  zsupssdc  10345  exbtwnzlemex  10356  uzsinds  10553  iseqovex  10567  seq3val  10569  seqvalcd  10570  seqf  10573  seqovcd  10576  monoord2  10595  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  seq3f1olemqsum  10622  seq3f1olemp  10624  seq3f1oleml  10625  seq3f1o  10626  nn0ltexp2  10818  bccl  10876  seq3shft  11020  caucvgre  11163  cvg1nlemcau  11166  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  cau3lem  11296  zsumdc  11566  fsum3  11569  isumz  11571  isumss2  11575  fsumsersdc  11577  fsum3ser  11579  fisum0diag2  11629  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratz  11714  mertenslem2  11718  mertensabs  11719  zproddc  11761  fprodseq  11765  prod1dc  11768  fprodsplitdc  11778  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemzz  12194  bezoutlemeu  12199  bezoutlemle  12200  dfgcd3  12202  prmind2  12313  sqrt2irr  12355  hashdvds  12414  ennnfoneleminc  12653  ennnfonelemex  12656  ennnfonelemr  12665  ctinfom  12670  ctinf  12672  ctiunctlemudc  12679  ssnnctlemct  12688  nninfdclemp1  12692  tgcn  14528  mulcncflem  14927  suplociccreex  14944  dedekindicc  14953  nnsf  15736  nninfsellemqall  15746  nninfomni  15750  trirec0  15775  apdiff  15779  iswomni0  15782  dceqnconst  15791  dcapnconst  15792  neap0mkv  15800  ltlenmkv  15801