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  5912  tfrlem1  6474  tfrlemiubacc  6496  tfrlemi1  6498  tfr1onlemubacc  6512  tfr1onlemaccex  6514  tfrcllembxssdm  6522  tfrcllemubacc  6525  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  rdgon  6552  frecfcllem  6570  frecsuclem  6572  nneneq  7043  fimax2gtrilemstep  7090  supubti  7198  suplubti  7199  finomni  7339  nninfwlporlemd  7371  nninfinfwlpo  7379  acfun  7422  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  ccfunen  7483  cc2  7486  cauappcvgprlemladdrl  7877  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgsrlembound  8014  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  suplocsrlem  8028  peano5nnnn  8112  axcaucvglemres  8119  axpre-suploc  8122  suprleubex  9134  nnsub  9182  supinfneg  9829  infsupneg  9830  infregelbex  9832  ublbneg  9847  zsupssdc  10499  exbtwnzlemex  10510  uzsinds  10707  iseqovex  10721  seq3val  10723  seqvalcd  10724  seqf  10727  seqovcd  10730  monoord2  10749  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seq3f1olemqsum  10776  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  nn0ltexp2  10972  bccl  11030  seq3shft  11403  caucvgre  11546  cvg1nlemcau  11549  resqrexlemglsq  11587  resqrexlemsqa  11589  resqrexlemex  11590  cau3lem  11679  zsumdc  11950  fsum3  11953  isumz  11955  isumss2  11959  fsumsersdc  11961  fsum3ser  11963  fisum0diag2  12013  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratz  12098  mertenslem2  12102  mertensabs  12103  zproddc  12145  fprodseq  12149  prod1dc  12152  fprodsplitdc  12162  bezoutlemmain  12574  bezoutlemex  12577  bezoutlemzz  12578  bezoutlemeu  12583  bezoutlemle  12584  dfgcd3  12586  prmind2  12697  sqrt2irr  12739  hashdvds  12798  ennnfoneleminc  13037  ennnfonelemex  13040  ennnfonelemr  13049  ctinfom  13054  ctinf  13056  ctiunctlemudc  13063  ssnnctlemct  13072  nninfdclemp1  13076  mplsubgfilemcl  14719  tgcn  14938  mulcncflem  15337  suplociccreex  15354  dedekindicc  15363  vtxedgfi  16146  vtxlpfi  16147  nnsf  16633  nninfsellemqall  16643  nninfomni  16647  trirec0  16674  apdiff  16678  iswomni0  16682  dceqnconst  16691  dcapnconst  16692  neap0mkv  16700  ltlenmkv  16701