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

Theorem cbvalv 2260
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2005. (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 1829 . . . 4 𝑦𝜑
21nfal 2138 . . 3 𝑦𝑥𝜑
3 cbvalv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43spv 2247 . . 3 (∀𝑥𝜑𝜓)
52, 4alrimi 2068 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
6 nfv 1829 . . . 4 𝑥𝜓
76nfal 2138 . . 3 𝑥𝑦𝜓
83equcoms 1933 . . . . 5 (𝑦 = 𝑥 → (𝜑𝜓))
98bicomd 211 . . . 4 (𝑦 = 𝑥 → (𝜓𝜑))
109spv 2247 . . 3 (∀𝑦𝜓𝜑)
117, 10alrimi 2068 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
125, 11impbii 197 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1700
This theorem is referenced by:  cbvexv  2262  cbvaldva  2268  cbval2v  2272  nfcjust  2738  cdeqal1  3392  zfpow  4764  tfisi  6927  pssnn  8040  findcard  8061  findcard3  8065  zfinf  8396  aceq0  8801  kmlem1  8832  kmlem13  8844  fin23lem32  9026  fin23lem41  9034  zfac  9142  zfcndpow  9294  zfcndinf  9296  zfcndac  9297  axgroth4  9510  relexpindlem  13599  ramcl  15519  mreexexlemd  16075  bnj1112  30098  dfon2lem6  30730  dfon2lem7  30731  dfon2  30734  phpreu  32346  axc11n-16  33024  dfac11  36433
  Copyright terms: Public domain W3C validator