Theorem cbvex 2022

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
cbval.1
cbval.2
cbval.3

Assertion

Ref	Expression
cbvex

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbval.1	. . . . 5
2	1	nfn 1901	. . . 4
3		cbval.2	. . . . 5
4	3	nfn 1901	. . . 4
5		cbval.3	. . . . 5
6	5	notbid 294	. . . 4
7	2, 4, 6	cbval 2021	. . 3
8	7	notbii 296	. 2
9		df-ex 1613	. 2
10		df-ex 1613	. 2
11	8, 9, 10	3bitr4i 277	1

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

This theorem is referenced by:  cbvexv  2024  cbvex2OLD  2029  sb8e  2168  exsb  2212  euf  2292  mo2  2293  cbvmo  2322  clelab  2601  clelabOLD  2602  issetf  3114  eqvincf  3227  rexab2  3266  euabsn  4102  eluniab  4260  cbvopab1  4522  cbvopab2  4523  cbvopab1s  4524  axrep1  4564  axrep2  4565  axrep4  4567  opeliunxp  5056  dfdmf  5201  dfrnf  5246  elrnmpt1  5256  cbvoprab1  6369  cbvoprab2  6370  opabex3d  6778  opabex3  6779  zfcndrep  9013  fsum2dlem  13585  fprod2dlem  13784  sbcexf  30518  elunif  31391  stoweidlem46  31828  opeliun2xp  32922  bnj1146  33850  bnj607  33974  bnj1228  34067

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