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

Theorem cbvab 2564
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
Hypotheses
Ref Expression
cbvab.1
cbvab.2
cbvab.3
Assertion
Ref Expression
cbvab

Proof of Theorem cbvab
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cbvab.1 . . . . 5
21sbco2 2210 . . . 4
3 cbvab.2 . . . . . 6
4 cbvab.3 . . . . . 6
53, 4sbie 2203 . . . . 5
65sbbii 1794 . . . 4
72, 6bitr3i 255 . . 3
8 df-clab 2409 . . 3
9 df-clab 2409 . . 3
107, 8, 93bitr4i 281 . 2
1110eqriv 2419 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wceq 1438  wnf 1664  wsb 1787   wcel 1869  cab 2408 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415 This theorem is referenced by:  cbvabv  2566  cbvrab  3080  cbvsbc  3329  cbvrabcsf  3431  rabsnifsb  4066  rabasiun  4301  dfdmf  5045  dfrnf  5090  funfv2f  5948  abrexex2g  6782  abrexex2  6786  bnj873  29737  ptrest  31859  poimirlem26  31886  poimirlem27  31887
 Copyright terms: Public domain W3C validator