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

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
StepHypRef Expression
1 cbval.1 . . . . 5
21nfn 1901 . . . 4
3 cbval.2 . . . . 5
43nfn 1901 . . . 4
5 cbval.3 . . . . 5
65notbid 294 . . . 4
72, 4, 6cbval 2021 . . 3
87notbii 296 . 2
9 df-ex 1613 . 2
10 df-ex 1613 . 2
118, 9, 103bitr4i 277 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator