Theorem cbvex 1162

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 1001	. . . 4 |- (-. ph -> A.y -. ph)
3		cbvex.2	. . . . 5 |- (ps -> A.xps)
4	3	hbn 1001	. . . 4 |- (-. ps -> A.x -. ps)
5		cbvex.3	. . . . 5 |- (x = y -> (ph <-> ps))
6	5	negbid 609	. . . 4 |- (x = y -> (-. ph <-> -. ps))
7	2, 4, 6	cbval 1161	. . 3 |- (A.x -. ph <-> A.y -. ps)
8	7	negbii 187	. 2 |- (-. A.x -. ph <-> -. A.y -. ps)
9		df-ex 978	. 2 |- (E.xph <-> -. A.x -. ph)
10		df-ex 978	. 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 951   = wceq 953  E.wex 977

This theorem is referenced by:  cbvexv 1310  cbvex2 1312  sb7f 1336  euf 1377  mo 1386  cbvmo 1401  mopick 1426  clelab 1573  cbvrex 1790  vtoclgf 1837  cla4gf 1851  eqvincf 1875  abn0 2280  eusn 2436  eluniab 2503  cbvopab1 2664  cbvopab1s 2665  axrep1 2684  axrep2 2685  axrep4 2687  opabid 2799  reusn 2882  dfdmf 3295  dfrnf 3334  zfcndrep 4938  nnwof 6391  cbvrexf 10338

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

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

Copyright terms: Public domain