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

Theorem cbvalv 2309
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2059. (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 1879 . . . 4 (𝜑 → ∀𝑦𝜑)
21hbal 2076 . . 3 (∀𝑥𝜑 → ∀𝑦𝑥𝜑)
3 cbvalv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43spv 2296 . . 3 (∀𝑥𝜑𝜓)
52, 4alrimih 1791 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
6 ax-5 1879 . . . 4 (𝜓 → ∀𝑥𝜓)
76hbal 2076 . . 3 (∀𝑦𝜓 → ∀𝑥𝑦𝜓)
83equcoms 1993 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
98bicomd 213 . . . 4 (𝑦 = 𝑥 → (𝜓𝜑))
109spv 2296 . . 3 (∀𝑦𝜓𝜑)
117, 10alrimih 1791 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
125, 11impbii 199 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-11 2074  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745
This theorem is referenced by:  cbvexv  2311  cbvaldva  2317  cbval2v  2321  nfcjust  2781  cdeqal1  3459  zfpow  4874  tfisi  7100  pssnn  8219  findcard  8240  findcard3  8244  zfinf  8574  aceq0  8979  kmlem1  9010  kmlem13  9022  fin23lem32  9204  fin23lem41  9212  zfac  9320  zfcndpow  9476  zfcndinf  9478  zfcndac  9479  axgroth4  9692  relexpindlem  13847  ramcl  15780  mreexexlemd  16351  bnj1112  31177  dfon2lem6  31817  dfon2lem7  31818  dfon2  31821  phpreu  33523  axc11n-16  34542  dfac11  37949
  Copyright terms: Public domain W3C validator