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

Theorem cbval 2021
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
cbval.1
cbval.2
cbval.3
Assertion
Ref Expression
cbval

Proof of Theorem cbval
StepHypRef Expression
1 cbval.1 . . 3
2 cbval.2 . . 3
3 cbval.3 . . . 4
43biimpd 207 . . 3
51, 2, 4cbv3 2015 . 2
63biimprd 223 . . . 4
76equcoms 1795 . . 3
82, 1, 7cbv3 2015 . 2
95, 8impbii 188 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  F/wnf 1616 This theorem is referenced by:  cbvex  2022  cbvalv  2023  cbval2  2027  sb8  2167  sb8eu  2318  sb8euOLD  2319  cleqh  2572  abbiOLD  2589  cleqfOLD  2647  cbvralf  3078  ralab2  3264  cbvralcsf  3466  dfss2f  3494  elintab  4297  reusv2lem4  4656  cbviota  5561  sb8iota  5563  dffun6f  5607  findcard2  7780  aceq1  8519  sbcalf  30517  alrimii  30524  aomclem6  31005  stoweidlem34  31816  bnj1385  33891  bnj1476  33905 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