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

Theorem cbvralv 2583
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 1462 . 2 𝑦𝜑
2 nfv 1462 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 2579 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wral 2353
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 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358
This theorem is referenced by:  cbvral2v  2591  cbvral3v  2593  reu7  2798  reusv3i  4245  omsinds  4398  cnvpom  4927  f1mpt  5490  grprinvlem  5774  grprinvd  5775  tfrlem1  6005  tfrlemiubacc  6027  tfrlemi1  6029  tfr1onlemubacc  6043  tfr1onlemaccex  6045  tfrcllembxssdm  6053  tfrcllemubacc  6056  tfrcllemaccex  6058  tfrcllemres  6059  tfrcldm  6060  rdgon  6083  frecfcllem  6101  frecsuclem  6103  nneneq  6503  supubti  6601  suplubti  6602  finomni  6701  cauappcvgprlemladdrl  7119  caucvgprlemcl  7138  caucvgprlemladdrl  7140  caucvgsrlembound  7242  caucvgsrlemgt1  7243  caucvgsrlemoffres  7248  peano5nnnn  7330  axcaucvglemres  7337  suprleubex  8309  nnsub  8354  supinfneg  8978  infsupneg  8979  ublbneg  8993  exbtwnzlemex  9550  uzsinds  9737  iseqovex  9748  iseqval  9749  iseqvalt  9751  iseqfclt  9755  monoord2  9771  bccl  10010  caucvgre  10241  cvg1nlemcau  10244  resqrexlemglsq  10282  resqrexlemsqa  10284  resqrexlemex  10285  cau3lem  10374  bezoutlemmain  10767  bezoutlemex  10770  bezoutlemzz  10771  bezoutlemeu  10776  bezoutlemle  10777  dfgcd3  10779  prmind2  10882  sqrt2irr  10921  hashdvds  10977
  Copyright terms: Public domain W3C validator