Theorem cbvralv 2737

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

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

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488

This theorem is referenced by:  cbvral2v  2750  cbvral3v  2752  reu7  2967  reusv3i  4505  omsinds  4669  cnvpom  5224  f1mpt  5839  tfrlem1  6393  tfrlemiubacc  6415  tfrlemi1  6417  tfr1onlemubacc  6431  tfr1onlemaccex  6433  tfrcllembxssdm  6441  tfrcllemubacc  6444  tfrcllemaccex  6446  tfrcllemres  6447  tfrcldm  6448  rdgon  6471  frecfcllem  6489  frecsuclem  6491  nneneq  6953  fimax2gtrilemstep  6996  supubti  7100  suplubti  7101  finomni  7241  nninfwlporlemd  7273  nninfinfwlpo  7281  acfun  7318  exmidontriimlem3  7334  exmidontriimlem4  7335  exmidontriim  7336  ccfunen  7375  cc2  7378  cauappcvgprlemladdrl  7769  caucvgprlemcl  7788  caucvgprlemladdrl  7790  caucvgsrlembound  7906  caucvgsrlemgt1  7907  caucvgsrlemoffres  7912  suplocsrlem  7920  peano5nnnn  8004  axcaucvglemres  8011  axpre-suploc  8014  suprleubex  9026  nnsub  9074  supinfneg  9715  infsupneg  9716  infregelbex  9718  ublbneg  9733  zsupssdc  10379  exbtwnzlemex  10390  uzsinds  10587  iseqovex  10601  seq3val  10603  seqvalcd  10604  seqf  10607  seqovcd  10610  monoord2  10629  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  seq3f1olemqsum  10656  seq3f1olemp  10658  seq3f1oleml  10659  seq3f1o  10660  nn0ltexp2  10852  bccl  10910  seq3shft  11091  caucvgre  11234  cvg1nlemcau  11237  resqrexlemglsq  11275  resqrexlemsqa  11277  resqrexlemex  11278  cau3lem  11367  zsumdc  11637  fsum3  11640  isumz  11642  isumss2  11646  fsumsersdc  11648  fsum3ser  11650  fisum0diag2  11700  cvgratnnlemnexp  11777  cvgratnnlemmn  11778  cvgratz  11785  mertenslem2  11789  mertensabs  11790  zproddc  11832  fprodseq  11836  prod1dc  11839  fprodsplitdc  11849  bezoutlemmain  12261  bezoutlemex  12264  bezoutlemzz  12265  bezoutlemeu  12270  bezoutlemle  12271  dfgcd3  12273  prmind2  12384  sqrt2irr  12426  hashdvds  12485  ennnfoneleminc  12724  ennnfonelemex  12727  ennnfonelemr  12736  ctinfom  12741  ctinf  12743  ctiunctlemudc  12750  ssnnctlemct  12759  nninfdclemp1  12763  mplsubgfilemcl  14403  tgcn  14622  mulcncflem  15021  suplociccreex  15038  dedekindicc  15047  nnsf  15875  nninfsellemqall  15885  nninfomni  15889  trirec0  15916  apdiff  15920  iswomni0  15923  dceqnconst  15932  dcapnconst  15933  neap0mkv  15941  ltlenmkv  15942