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

Theorem cbvald 2408
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2452. Usage of this theorem is discouraged because it depends on ax-13 2373. See cbvaldw 2338 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2373. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.)
Hypotheses
Ref Expression
cbvald.1 𝑦𝜑
cbvald.2 (𝜑 → Ⅎ𝑦𝜓)
cbvald.3 (𝜑 → (𝑥 = 𝑦 → (𝜓𝜒)))
Assertion
Ref Expression
cbvald (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)   𝜒(𝑦)

Proof of Theorem cbvald
StepHypRef Expression
1 nfv 1920 . 2 𝑥𝜑
2 cbvald.1 . 2 𝑦𝜑
3 cbvald.2 . 2 (𝜑 → Ⅎ𝑦𝜓)
4 nfvd 1921 . 2 (𝜑 → Ⅎ𝑥𝜒)
5 cbvald.3 . 2 (𝜑 → (𝑥 = 𝑦 → (𝜓𝜒)))
61, 2, 3, 4, 5cbv2 2404 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539  wnf 1789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-11 2157  ax-12 2174  ax-13 2373
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-nf 1790
This theorem is referenced by:  cbvexd  2409  cbvaldva  2410  axextnd  10331  axrepndlem1  10332  axunndlem1  10335  axpowndlem2  10338  axpowndlem3  10339  axpowndlem4  10340  axregndlem2  10343  axregnd  10344  axinfnd  10346  axacndlem5  10351  axacnd  10352  axextdist  33754  distel  33758  wl-sb8eut  35711
  Copyright terms: Public domain W3C validator