Theorem cbvralv 2765

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

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

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  cbvral2v  2778  cbvral3v  2780  reu7  2998  reusv3i  4549  omsinds  4713  cnvpom  5270  f1mpt  5894  tfrlem1  6452  tfrlemiubacc  6474  tfrlemi1  6476  tfr1onlemubacc  6490  tfr1onlemaccex  6492  tfrcllembxssdm  6500  tfrcllemubacc  6503  tfrcllemaccex  6505  tfrcllemres  6506  tfrcldm  6507  rdgon  6530  frecfcllem  6548  frecsuclem  6550  nneneq  7014  fimax2gtrilemstep  7058  supubti  7162  suplubti  7163  finomni  7303  nninfwlporlemd  7335  nninfinfwlpo  7343  acfun  7385  exmidontriimlem3  7401  exmidontriimlem4  7402  exmidontriim  7403  ccfunen  7446  cc2  7449  cauappcvgprlemladdrl  7840  caucvgprlemcl  7859  caucvgprlemladdrl  7861  caucvgsrlembound  7977  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  suplocsrlem  7991  peano5nnnn  8075  axcaucvglemres  8082  axpre-suploc  8085  suprleubex  9097  nnsub  9145  supinfneg  9786  infsupneg  9787  infregelbex  9789  ublbneg  9804  zsupssdc  10453  exbtwnzlemex  10464  uzsinds  10661  iseqovex  10675  seq3val  10677  seqvalcd  10678  seqf  10681  seqovcd  10684  monoord2  10703  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  seq3f1olemqsum  10730  seq3f1olemp  10732  seq3f1oleml  10733  seq3f1o  10734  nn0ltexp2  10926  bccl  10984  seq3shft  11344  caucvgre  11487  cvg1nlemcau  11490  resqrexlemglsq  11528  resqrexlemsqa  11530  resqrexlemex  11531  cau3lem  11620  zsumdc  11890  fsum3  11893  isumz  11895  isumss2  11899  fsumsersdc  11901  fsum3ser  11903  fisum0diag2  11953  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratz  12038  mertenslem2  12042  mertensabs  12043  zproddc  12085  fprodseq  12089  prod1dc  12092  fprodsplitdc  12102  bezoutlemmain  12514  bezoutlemex  12517  bezoutlemzz  12518  bezoutlemeu  12523  bezoutlemle  12524  dfgcd3  12526  prmind2  12637  sqrt2irr  12679  hashdvds  12738  ennnfoneleminc  12977  ennnfonelemex  12980  ennnfonelemr  12989  ctinfom  12994  ctinf  12996  ctiunctlemudc  13003  ssnnctlemct  13012  nninfdclemp1  13016  mplsubgfilemcl  14657  tgcn  14876  mulcncflem  15275  suplociccreex  15292  dedekindicc  15301  nnsf  16330  nninfsellemqall  16340  nninfomni  16344  trirec0  16371  apdiff  16375  iswomni0  16378  dceqnconst  16387  dcapnconst  16388  neap0mkv  16396  ltlenmkv  16397