Theorem cbvralv 2768

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

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

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516

This theorem is referenced by:  cbvral2v  2781  cbvral3v  2783  reu7  3002  reusv3i  4562  omsinds  4726  cnvpom  5286  f1mpt  5922  tfrlem1  6517  tfrlemiubacc  6539  tfrlemi1  6541  tfr1onlemubacc  6555  tfr1onlemaccex  6557  tfrcllembxssdm  6565  tfrcllemubacc  6568  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  rdgon  6595  frecfcllem  6613  frecsuclem  6615  nneneq  7086  fimax2gtrilemstep  7133  supubti  7241  suplubti  7242  finomni  7382  nninfwlporlemd  7414  nninfinfwlpo  7422  acfun  7465  exmidontriimlem3  7481  exmidontriimlem4  7482  exmidontriim  7483  ccfunen  7526  cc2  7529  cauappcvgprlemladdrl  7920  caucvgprlemcl  7939  caucvgprlemladdrl  7941  caucvgsrlembound  8057  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  suplocsrlem  8071  peano5nnnn  8155  axcaucvglemres  8162  axpre-suploc  8165  suprleubex  9176  nnsub  9224  supinfneg  9873  infsupneg  9874  infregelbex  9876  ublbneg  9891  zsupssdc  10544  exbtwnzlemex  10555  uzsinds  10752  iseqovex  10766  seq3val  10768  seqvalcd  10769  seqf  10772  seqovcd  10775  monoord2  10794  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seq3f1olemqsum  10821  seq3f1olemp  10823  seq3f1oleml  10824  seq3f1o  10825  nn0ltexp2  11017  bccl  11075  seq3shft  11461  caucvgre  11604  cvg1nlemcau  11607  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  cau3lem  11737  zsumdc  12008  fsum3  12011  isumz  12013  isumss2  12017  fsumsersdc  12019  fsum3ser  12021  fisum0diag2  12071  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratz  12156  mertenslem2  12160  mertensabs  12161  zproddc  12203  fprodseq  12207  prod1dc  12210  fprodsplitdc  12220  bezoutlemmain  12632  bezoutlemex  12635  bezoutlemzz  12636  bezoutlemeu  12641  bezoutlemle  12642  dfgcd3  12644  prmind2  12755  sqrt2irr  12797  hashdvds  12856  ennnfoneleminc  13095  ennnfonelemex  13098  ennnfonelemr  13107  ctinfom  13112  ctinf  13114  ctiunctlemudc  13121  ssnnctlemct  13130  nninfdclemp1  13134  mplsubgfilemcl  14783  tgcn  15002  mulcncflem  15401  suplociccreex  15418  dedekindicc  15427  vtxedgfi  16213  vtxlpfi  16214  nnsf  16714  nninfsellemqall  16724  nninfomni  16728  repiecef  16743  trirec0  16759  apdiff  16763  iswomni0  16767  dceqnconst  16776  dcapnconst  16777  neap0mkv  16785  ltlenmkv  16786