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

Theorem cbvald 2400
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2444. Usage of this theorem is discouraged because it depends on ax-13 2365. See cbvaldw 2328 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2365. (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 1909 . 2 𝑥𝜑
2 cbvald.1 . 2 𝑦𝜑
3 cbvald.2 . 2 (𝜑 → Ⅎ𝑦𝜓)
4 nfvd 1910 . 2 (𝜑 → Ⅎ𝑥𝜒)
5 cbvald.3 . 2 (𝜑 → (𝑥 = 𝑦 → (𝜓𝜒)))
61, 2, 3, 4, 5cbv2 2396 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1531  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-11 2146  ax-12 2166  ax-13 2365
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778
This theorem is referenced by:  cbvexd  2401  cbvaldva  2402  axextnd  10616  axrepndlem1  10617  axunndlem1  10620  axpowndlem2  10623  axpowndlem3  10624  axpowndlem4  10625  axregndlem2  10628  axregnd  10629  axinfnd  10631  axacndlem5  10636  axacnd  10637  axextdist  35523  distel  35527  wl-sb8eut  37173
  Copyright terms: Public domain W3C validator