This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gencbval

Description: Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996)

Ref Expression
Hypotheses gencbval.1 
|- A e. _V
gencbval.2 
|- ( A = y -> ( ph <-> ps ) )
gencbval.3 
|- ( A = y -> ( ch <-> th ) )
gencbval.4 
|- ( th <-> E. x ( ch /\ A = y ) )
Assertion gencbval 
|- ( A. x ( ch -> ph ) <-> A. y ( th -> ps ) )

Proof

Step Hyp Ref Expression
1 gencbval.1 
 |-  A e. _V
2 gencbval.2 
 |-  ( A = y -> ( ph <-> ps ) )
3 gencbval.3 
 |-  ( A = y -> ( ch <-> th ) )
4 gencbval.4 
 |-  ( th <-> E. x ( ch /\ A = y ) )
5 2 notbid 
 |-  ( A = y -> ( -. ph <-> -. ps ) )
6 1 5 3 4 gencbvex 
 |-  ( E. x ( ch /\ -. ph ) <-> E. y ( th /\ -. ps ) )
7 exanali 
 |-  ( E. x ( ch /\ -. ph ) <-> -. A. x ( ch -> ph ) )
8 exanali 
 |-  ( E. y ( th /\ -. ps ) <-> -. A. y ( th -> ps ) )
9 6 7 8 3bitr3i 
 |-  ( -. A. x ( ch -> ph ) <-> -. A. y ( th -> ps ) )
10 9 con4bii 
 |-  ( A. x ( ch -> ph ) <-> A. y ( th -> ps ) )