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

Theorem cbvralv 2629
 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 1491 . 2 𝑦𝜑
2 nfv 1491 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 2625 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2391 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396 This theorem is referenced by:  cbvral2v  2637  cbvral3v  2639  reu7  2850  reusv3i  4348  omsinds  4503  cnvpom  5049  f1mpt  5638  grprinvlem  5931  grprinvd  5932  tfrlem1  6171  tfrlemiubacc  6193  tfrlemi1  6195  tfr1onlemubacc  6209  tfr1onlemaccex  6211  tfrcllembxssdm  6219  tfrcllemubacc  6222  tfrcllemaccex  6224  tfrcllemres  6225  tfrcldm  6226  rdgon  6249  frecfcllem  6267  frecsuclem  6269  nneneq  6717  fimax2gtrilemstep  6760  supubti  6852  suplubti  6853  finomni  6978  acfun  7027  ccfunen  7043  cauappcvgprlemladdrl  7429  caucvgprlemcl  7448  caucvgprlemladdrl  7450  caucvgsrlembound  7566  caucvgsrlemgt1  7567  caucvgsrlemoffres  7572  suplocsrlem  7580  peano5nnnn  7664  axcaucvglemres  7671  axpre-suploc  7674  suprleubex  8669  nnsub  8716  supinfneg  9339  infsupneg  9340  ublbneg  9354  exbtwnzlemex  9967  uzsinds  10155  iseqovex  10169  seq3val  10171  seqvalcd  10172  seqf  10174  seqovcd  10176  monoord2  10190  iseqf1olemjpcl  10208  iseqf1olemqpcl  10209  seq3f1olemqsum  10213  seq3f1olemp  10215  seq3f1oleml  10216  seq3f1o  10217  bccl  10453  seq3shft  10550  caucvgre  10693  cvg1nlemcau  10696  resqrexlemglsq  10734  resqrexlemsqa  10736  resqrexlemex  10737  cau3lem  10826  zsumdc  11093  fsum3  11096  isumz  11098  isumss2  11102  fsumsersdc  11104  fsum3ser  11106  fisum0diag2  11156  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  cvgratz  11241  mertenslem2  11245  mertensabs  11246  bezoutlemmain  11582  bezoutlemex  11585  bezoutlemzz  11586  bezoutlemeu  11591  bezoutlemle  11592  dfgcd3  11594  prmind2  11697  sqrt2irr  11736  hashdvds  11792  ennnfoneleminc  11819  ennnfonelemex  11822  ennnfonelemr  11831  ctinfom  11836  ctinf  11838  ctiunctlemudc  11845  tgcn  12272  mulcncflem  12654  suplociccreex  12666  nnsf  13010  nninfsellemqall  13022  nninfomni  13026
 Copyright terms: Public domain W3C validator