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

Theorem cbval 1685
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 1458 . 2 (𝜑 → ∀𝑦𝜑)
3 cbval.2 . . 3 𝑥𝜓
43nfri 1458 . 2 (𝜓 → ∀𝑥𝜓)
5 cbval.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
62, 4, 5cbvalh 1684 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1288  wnf 1395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473
This theorem depends on definitions:  df-bi 116  df-nf 1396
This theorem is referenced by:  sb8  1785  cbval2  1845  sb8eu  1962  abbi  2202  cleqf  2253  cbvralf  2585  ralab2  2780  cbvralcsf  2991  dfss2f  3017  elintab  3705  cbviota  4998  sb8iota  5000  dffun6f  5041  dffun4f  5044  mptfvex  5401  findcard2  6659  findcard2s  6660
  Copyright terms: Public domain W3C validator