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

Step	Hyp	Ref	Expression
1		cbval.1	. . 3
2		cbval.2	. . 3
3		cbval.3	. . . 4
4	3	biimpd 207	. . 3
5	1, 2, 4	cbv3 2015	. 2
6	3	biimprd 223	. . . 4
7	6	equcoms 1795	. . 3
8	2, 1, 7	cbv3 2015	. 2
9	5, 8	impbii 188	1

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