Theorem cbvex 1166

Description: Rule used to change bound variables with implicit substitution.

Hypotheses

Ref	Expression
cbvex.1	|- (ph -> A.yph)
cbvex.2	|- (ps -> A.xps)
cbvex.3	|- (x = y -> (ph <-> ps))

Assertion

Ref	Expression
cbvex	|- (E.xph <-> E.yps)

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbvex.1	. . . . 5 |- (ph -> A.yph)
2	1	hbn 1004	. . . 4 |- (-. ph -> A.y -. ph)
3		cbvex.2	. . . . 5 |- (ps -> A.xps)
4	3	hbn 1004	. . . 4 |- (-. ps -> A.x -. ps)
5		cbvex.3	. . . . 5 |- (x = y -> (ph <-> ps))
6	5	negbid 611	. . . 4 |- (x = y -> (-. ph <-> -. ps))
7	2, 4, 6	cbval 1165	. . 3 |- (A.x -. ph <-> A.y -. ps)
8	7	negbii 187	. 2 |- (-. A.x -. ph <-> -. A.y -. ps)
9		df-ex 981	. 2 |- (E.xph <-> -. A.x -. ph)
10		df-ex 981	. 2 |- (E.yps <-> -. A.y -. ps)
11	8, 9, 10	3bitr4 183	1 |- (E.xph <-> E.yps)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146  A.wal 954   = wceq 956  E.wex 980

This theorem is referenced by:  cbvexv 1315  cbvex2 1317  sb7f 1341  euf 1384  mo 1393  cbvmo 1408  mopick 1433  clelab 1581  cbvrexf 1797  cbvrex 1799  vtoclgf 1846  cla4gf 1860  eqvincf 1884  abn0 2290  eusn 2446  eluniab 2513  cbvopab1 2674  cbvopab1s 2675  axrep1 2694  axrep2 2695  axrep4 2697  opabid 2810  reusn 2892  dfdmf 3306  dfrnf 3348  zfcndrep 4966  nnwof 6459

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981

Copyright terms: Public domain