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

Theorem cbvalv 2261
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2006. (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 nfv 1830 . . . 4 𝑦𝜑
21nfal 2139 . . 3 𝑦𝑥𝜑
3 cbvalv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43spv 2248 . . 3 (∀𝑥𝜑𝜓)
52, 4alrimi 2069 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
6 nfv 1830 . . . 4 𝑥𝜓
76nfal 2139 . . 3 𝑥𝑦𝜓
83equcoms 1934 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
98bicomd 212 . . . 4 (𝑦 = 𝑥 → (𝜓𝜑))
109spv 2248 . . 3 (∀𝑦𝜓𝜑)
117, 10alrimi 2069 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
125, 11impbii 198 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701 This theorem is referenced by:  cbvexv  2263  cbvaldva  2269  cbval2v  2273  nfcjust  2739  cdeqal1  3393  zfpow  4770  tfisi  6950  pssnn  8063  findcard  8084  findcard3  8088  zfinf  8419  aceq0  8824  kmlem1  8855  kmlem13  8867  fin23lem32  9049  fin23lem41  9057  zfac  9165  zfcndpow  9317  zfcndinf  9319  zfcndac  9320  axgroth4  9533  relexpindlem  13651  ramcl  15571  mreexexlemd  16127  bnj1112  30305  dfon2lem6  30937  dfon2lem7  30938  dfon2  30941  phpreu  32563  axc11n-16  33241  dfac11  36650
 Copyright terms: Public domain W3C validator