Theorem cbvex2 2028

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 16-Jun-2019.)

Hypotheses

Ref	Expression
cbval2.1
cbval2.2
cbval2.3
cbval2.4
cbval2.5

Assertion

Ref	Expression
cbvex2

Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem cbvex2

Step	Hyp	Ref	Expression
1		cbval2.1	. . . . 5
2	1	nfn 1901	. . . 4
3		cbval2.2	. . . . 5
4	3	nfn 1901	. . . 4
5		cbval2.3	. . . . 5
6	5	nfn 1901	. . . 4
7		cbval2.4	. . . . 5
8	7	nfn 1901	. . . 4
9		cbval2.5	. . . . 5
10	9	notbid 294	. . . 4
11	2, 4, 6, 8, 10	cbval2 2027	. . 3
12	11	notbii 296	. 2
13		2exnaln 1650	. 2
14		2exnaln 1650	. 2
15	12, 13, 14	3bitr4i 277	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  F/wnf 1616

This theorem is referenced by:  cbvex2v  2031  2eu6OLD  2384  cbvopab  4520  cbvoprab12  6371

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