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

Theorem cbvald 2313
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2368. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
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 1883 . 2 𝑥𝜑
2 cbvald.1 . 2 𝑦𝜑
3 cbvald.2 . 2 (𝜑 → Ⅎ𝑦𝜓)
4 nfvd 1884 . 2 (𝜑 → Ⅎ𝑥𝜒)
5 cbvald.3 . 2 (𝜑 → (𝑥 = 𝑦 → (𝜓𝜒)))
61, 2, 3, 4, 5cbv2 2306 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521  wnf 1748
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-10 2059  ax-11 2074  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by:  cbvexd  2314  cbvaldvaOLD  2318  axextnd  9451  axrepndlem1  9452  axunndlem1  9455  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axregndlem2  9463  axregnd  9464  axinfnd  9466  axacndlem5  9471  axacnd  9472  axextdist  31829  distel  31833  wl-sb8eut  33489
  Copyright terms: Public domain W3C validator