MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvalv Structured version   Visualization version   GIF version

Theorem cbvalv 2382
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2132. (Revised by Wolf Lammen, 17-Jul-2021.)
Hypothesis
Ref Expression
cbvalv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvalv (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvalv
StepHypRef Expression
1 ax-5 1952 . . . 4 (𝜑 → ∀𝑦𝜑)
21hbal 2149 . . 3 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
3 cbvalv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43spv 2369 . . 3 (∀𝑥𝜑𝜓)
52, 4alrimih 1864 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
6 ax-5 1952 . . . 4 (𝜓 → ∀𝑥𝜓)
76hbal 2149 . . 3 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
83equcoms 2066 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
98bicomd 213 . . . 4 (𝑦 = 𝑥 → (𝜓𝜑))
109spv 2369 . . 3 (∀𝑦𝜓𝜑)
117, 10alrimih 1864 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
125, 11impbii 199 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-11 2147  ax-12 2160  ax-13 2355
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1818
This theorem is referenced by:  cbvexv  2384  cbvaldva  2390  cbval2v  2394  nfcjust  2854  cdeqal1  3532  zfpow  4949  tfisi  7175  pssnn  8294  findcard  8315  findcard3  8319  zfinf  8649  aceq0  9054  kmlem1  9085  kmlem13  9097  fin23lem32  9279  fin23lem41  9287  zfac  9395  zfcndpow  9551  zfcndinf  9553  zfcndac  9554  axgroth4  9767  relexpindlem  13923  ramcl  15856  mreexexlemd  16427  bnj1112  31279  dfon2lem6  31919  dfon2lem7  31920  dfon2  31923  phpreu  33625  axc11n-16  34644  dfac11  38051
  Copyright terms: Public domain W3C validator