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

Theorem cbvex4v 2034
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypotheses
Ref Expression
cbvex4v.1
cbvex4v.2 No typesetting for: |- ( ( z = f /\ w = g ) -> ( ps <-> ch ) )
Assertion
Ref Expression
cbvex4v No typesetting for: |- ( E. x E. y E. z E. w ph <-> E. v E. u E. f E. g ch )
Distinct variable groups:   , ,   , ,   , ,   f,g,   ,f   ,g   , , , , ,

Proof of Theorem cbvex4v
StepHypRef Expression
1 cbvex4v.1 . . . 4
212exbidv 1716 . . 3
32cbvex2v 2031 . 2
4 cbvex4v.2 . . . 4 No typesetting for: |- ( ( z = f /\ w = g ) -> ( ps <-> ch ) )
54cbvex2v 2031 . . 3 No typesetting for: |- ( E. z E. w ps <-> E. f E. g ch )
652exbii 1668 . 2 No typesetting for: |- ( E. v E. u E. z E. w ps <-> E. v E. u E. f E. g ch )
73, 6bitri 249 1 No typesetting for: |- ( E. x E. y E. z E. w ph <-> E. v E. u E. f E. g ch )
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  E.wex 1612
This theorem is referenced by:  addsrmo  9471  mulsrmo  9472
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