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

Theorem cbvralv 2550
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 1437 . 2 𝑦𝜑
2 nfv 1437 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 2546 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328
This theorem is referenced by:  cbvral2v  2558  cbvral3v  2560  reu7  2758  reusv3i  4218  cnvpom  4887  f1mpt  5437  grprinvlem  5722  grprinvd  5723  tfrlem1  5953  tfrlemiubacc  5974  tfrlemi1  5976  rdgon  6003  nneneq  6350  supubti  6404  suplubti  6405  cauappcvgprlemladdrl  6812  caucvgprlemcl  6831  caucvgprlemladdrl  6833  caucvgsrlembound  6935  caucvgsrlemgt1  6936  caucvgsrlemoffres  6941  peano5nnnn  7023  axcaucvglemres  7030  nnsub  8027  ublbneg  8644  iseqovex  9377  iseqval  9378  monoord2  9394  bccl  9628  caucvgre  9801  cvg1nlemcau  9804  resqrexlemglsq  9841  resqrexlemsqa  9843  resqrexlemex  9844  cau3lem  9933  sqrt2irr  10223
  Copyright terms: Public domain W3C validator