Theorem cbvralv 2767

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

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

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  cbvral2v  2780  cbvral3v  2782  reu7  3001  reusv3i  4556  omsinds  4720  cnvpom  5279  f1mpt  5911  tfrlem1  6473  tfrlemiubacc  6495  tfrlemi1  6497  tfr1onlemubacc  6511  tfr1onlemaccex  6513  tfrcllembxssdm  6521  tfrcllemubacc  6524  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  rdgon  6551  frecfcllem  6569  frecsuclem  6571  nneneq  7042  fimax2gtrilemstep  7089  supubti  7197  suplubti  7198  finomni  7338  nninfwlporlemd  7370  nninfinfwlpo  7378  acfun  7421  exmidontriimlem3  7437  exmidontriimlem4  7438  exmidontriim  7439  ccfunen  7482  cc2  7485  cauappcvgprlemladdrl  7876  caucvgprlemcl  7895  caucvgprlemladdrl  7897  caucvgsrlembound  8013  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  suplocsrlem  8027  peano5nnnn  8111  axcaucvglemres  8118  axpre-suploc  8121  suprleubex  9133  nnsub  9181  supinfneg  9828  infsupneg  9829  infregelbex  9831  ublbneg  9846  zsupssdc  10497  exbtwnzlemex  10508  uzsinds  10705  iseqovex  10719  seq3val  10721  seqvalcd  10722  seqf  10725  seqovcd  10728  monoord2  10747  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  seq3f1olemqsum  10774  seq3f1olemp  10776  seq3f1oleml  10777  seq3f1o  10778  nn0ltexp2  10970  bccl  11028  seq3shft  11398  caucvgre  11541  cvg1nlemcau  11544  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  cau3lem  11674  zsumdc  11944  fsum3  11947  isumz  11949  isumss2  11953  fsumsersdc  11955  fsum3ser  11957  fisum0diag2  12007  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratz  12092  mertenslem2  12096  mertensabs  12097  zproddc  12139  fprodseq  12143  prod1dc  12146  fprodsplitdc  12156  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemzz  12572  bezoutlemeu  12577  bezoutlemle  12578  dfgcd3  12580  prmind2  12691  sqrt2irr  12733  hashdvds  12792  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemr  13043  ctinfom  13048  ctinf  13050  ctiunctlemudc  13057  ssnnctlemct  13066  nninfdclemp1  13070  mplsubgfilemcl  14712  tgcn  14931  mulcncflem  15330  suplociccreex  15347  dedekindicc  15356  vtxedgfi  16139  vtxlpfi  16140  nnsf  16607  nninfsellemqall  16617  nninfomni  16621  trirec0  16648  apdiff  16652  iswomni0  16655  dceqnconst  16664  dcapnconst  16665  neap0mkv  16673  ltlenmkv  16674