ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvralv GIF version

Theorem cbvralv 2590
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
StepHypRef Expression
1 nfv 1466 . 2 𝑦𝜑
2 nfv 1466 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 2586 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364
This theorem is referenced by:  cbvral2v  2598  cbvral3v  2600  reu7  2810  reusv3i  4281  omsinds  4435  cnvpom  4973  f1mpt  5550  grprinvlem  5839  grprinvd  5840  tfrlem1  6073  tfrlemiubacc  6095  tfrlemi1  6097  tfr1onlemubacc  6111  tfr1onlemaccex  6113  tfrcllembxssdm  6121  tfrcllemubacc  6124  tfrcllemaccex  6126  tfrcllemres  6127  tfrcldm  6128  rdgon  6151  frecfcllem  6169  frecsuclem  6171  nneneq  6573  fimax2gtrilemstep  6616  supubti  6694  suplubti  6695  finomni  6796  cauappcvgprlemladdrl  7216  caucvgprlemcl  7235  caucvgprlemladdrl  7237  caucvgsrlembound  7339  caucvgsrlemgt1  7340  caucvgsrlemoffres  7345  peano5nnnn  7427  axcaucvglemres  7434  suprleubex  8415  nnsub  8461  supinfneg  9083  infsupneg  9084  ublbneg  9098  exbtwnzlemex  9661  uzsinds  9848  iseqovex  9870  iseqval  9871  iseqvalt  9873  seq3val  9874  iseqfclt  9879  seqf  9880  monoord2  9905  iseqf1olemjpcl  9924  iseqf1olemqpcl  9925  seq3f1olemqsum  9929  seq3f1olemp  9931  seq3f1oleml  9932  seq3f1o  9933  bccl  10175  seq3shft  10272  caucvgre  10414  cvg1nlemcau  10417  resqrexlemglsq  10455  resqrexlemsqa  10457  resqrexlemex  10458  cau3lem  10547  zisum  10774  fisum  10778  isumz  10781  isumss2  10785  fisumsers  10788  fisumser  10790  fisum0diag2  10841  cvgratnnlemnexp  10918  cvgratnnlemmn  10919  cvgratz  10926  mertenslem2  10930  mertensabs  10931  bezoutlemmain  11265  bezoutlemex  11268  bezoutlemzz  11269  bezoutlemeu  11274  bezoutlemle  11275  dfgcd3  11277  prmind2  11380  sqrt2irr  11419  hashdvds  11475  nnsf  11895  nninfsellemqall  11907  nninfomni  11911
  Copyright terms: Public domain W3C validator