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

Theorem cbval 1653
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
cbval.1 𝑦𝜑
cbval.2 𝑥𝜓
cbval.3 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbval (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Proof of Theorem cbval
StepHypRef Expression
1 cbval.1 . . 3 𝑦𝜑
21nfri 1428 . 2 (𝜑 → ∀𝑦𝜑)
3 cbval.2 . . 3 𝑥𝜓
43nfri 1428 . 2 (𝜓 → ∀𝑥𝜓)
5 cbval.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
62, 4, 5cbvalh 1652 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wal 1257  wnf 1365
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-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  sb8  1752  cbval2  1812  sb8eu  1929  abbi  2167  cleqf  2217  cbvralf  2544  ralab2  2727  cbvralcsf  2935  dfss2f  2963  elintab  3653  cbviota  4899  sb8iota  4901  dffun6f  4942  dffun4f  4945  mptfvex  5283  findcard2  6376  findcard2s  6377
  Copyright terms: Public domain W3C validator