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

Theorem cbval 1727
 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 1499 . 2 (𝜑 → ∀𝑦𝜑)
3 cbval.2 . . 3 𝑥𝜓
43nfri 1499 . 2 (𝜓 → ∀𝑥𝜓)
5 cbval.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
62, 4, 5cbvalh 1726 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1329  Ⅎwnf 1436 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-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1437 This theorem is referenced by:  sb8  1828  cbval2  1891  sb8eu  2010  abbi  2251  cleqf  2303  cbvralf  2646  ralab2  2843  cbvralcsf  3057  dfss2f  3083  elintab  3777  cbviota  5088  sb8iota  5090  dffun6f  5131  dffun4f  5134  mptfvex  5499  findcard2  6776  findcard2s  6777
 Copyright terms: Public domain W3C validator