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

Theorem cbvald 2412
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2456. Usage of this theorem is discouraged because it depends on ax-13 2377. See cbvaldw 2340 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2377. (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 1914 . 2 𝑥𝜑
2 cbvald.1 . 2 𝑦𝜑
3 cbvald.2 . 2 (𝜑 → Ⅎ𝑦𝜓)
4 nfvd 1915 . 2 (𝜑 → Ⅎ𝑥𝜒)
5 cbvald.3 . 2 (𝜑 → (𝑥 = 𝑦 → (𝜓𝜒)))
61, 2, 3, 4, 5cbv2 2408 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-11 2157  ax-12 2177  ax-13 2377
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  cbvexd  2413  cbvaldva  2414  axextnd  10631  axrepndlem1  10632  axunndlem1  10635  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axregndlem2  10643  axregnd  10644  axinfnd  10646  axacndlem5  10651  axacnd  10652  axextdist  35800  distel  35804  wl-sb8eut  37579
  Copyright terms: Public domain W3C validator