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

Theorem cbvald 2025
 Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2079. (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:   ,   ,

Proof of Theorem cbvald
StepHypRef Expression
1 nfv 1707 . 2
2 cbvald.1 . 2
3 cbvald.2 . 2
4 nfvd 1708 . 2
5 cbvald.3 . 2
61, 2, 3, 4, 5cbv2 2020 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  F/wnf 1616 This theorem is referenced by:  cbvexd  2026  cbvaldva  2032  axextnd  8987  axrepndlem1  8988  axunndlem1  8991  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axinfnd  9005  axacndlem5  9010  axacnd  9011  axextdist  29232  distel  29236  wl-sb8eut  30022 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator