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  4550  omsinds  4714  cnvpom  5271  f1mpt  5901  tfrlem1  6460  tfrlemiubacc  6482  tfrlemi1  6484  tfr1onlemubacc  6498  tfr1onlemaccex  6500  tfrcllembxssdm  6508  tfrcllemubacc  6511  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  rdgon  6538  frecfcllem  6556  frecsuclem  6558  nneneq  7026  fimax2gtrilemstep  7071  supubti  7177  suplubti  7178  finomni  7318  nninfwlporlemd  7350  nninfinfwlpo  7358  acfun  7400  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  ccfunen  7461  cc2  7464  cauappcvgprlemladdrl  7855  caucvgprlemcl  7874  caucvgprlemladdrl  7876  caucvgsrlembound  7992  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  suplocsrlem  8006  peano5nnnn  8090  axcaucvglemres  8097  axpre-suploc  8100  suprleubex  9112  nnsub  9160  supinfneg  9802  infsupneg  9803  infregelbex  9805  ublbneg  9820  zsupssdc  10470  exbtwnzlemex  10481  uzsinds  10678  iseqovex  10692  seq3val  10694  seqvalcd  10695  seqf  10698  seqovcd  10701  monoord2  10720  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seq3f1olemqsum  10747  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  nn0ltexp2  10943  bccl  11001  seq3shft  11364  caucvgre  11507  cvg1nlemcau  11510  resqrexlemglsq  11548  resqrexlemsqa  11550  resqrexlemex  11551  cau3lem  11640  zsumdc  11910  fsum3  11913  isumz  11915  isumss2  11919  fsumsersdc  11921  fsum3ser  11923  fisum0diag2  11973  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  cvgratz  12058  mertenslem2  12062  mertensabs  12063  zproddc  12105  fprodseq  12109  prod1dc  12112  fprodsplitdc  12122  bezoutlemmain  12534  bezoutlemex  12537  bezoutlemzz  12538  bezoutlemeu  12543  bezoutlemle  12544  dfgcd3  12546  prmind2  12657  sqrt2irr  12699  hashdvds  12758  ennnfoneleminc  12997  ennnfonelemex  13000  ennnfonelemr  13009  ctinfom  13014  ctinf  13016  ctiunctlemudc  13023  ssnnctlemct  13032  nninfdclemp1  13036  mplsubgfilemcl  14678  tgcn  14897  mulcncflem  15296  suplociccreex  15313  dedekindicc  15322  vtxedgfi  16048  vtxlpfi  16049  nnsf  16431  nninfsellemqall  16441  nninfomni  16445  trirec0  16472  apdiff  16476  iswomni0  16479  dceqnconst  16488  dcapnconst  16489  neap0mkv  16497  ltlenmkv  16498