Theorem cbvmowOLD

Description: Obsolete version of cbvmow as of 23-May-2024. (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvmowOLD.1	|- F/ y ph
	cbvmowOLD.2	|- F/ x ps
	cbvmowOLD.3	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvmowOLD	|- ( E* x ph <-> E* y ps )

Proof

Step	Hyp	Ref	Expression
1		cbvmowOLD.1	|- F/ y ph
2		cbvmowOLD.2	|- F/ x ps
3		cbvmowOLD.3	|- ( x = y -> ( ph <-> ps ) )
4	1	sb8ev	|- ( E. x ph <-> E. y [ y / x ] ph )
5	1	sb8euv	|- ( E! x ph <-> E! y [ y / x ] ph )
6	4 5	imbi12i	|- ( ( E. x ph -> E! x ph ) <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) )
7		moeu	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
8		moeu	|- ( E* y [ y / x ] ph <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) )
9	6 7 8	3bitr4i	|- ( E* x ph <-> E* y [ y / x ] ph )
10	2 3	sbiev	|- ( [ y / x ] ph <-> ps )
11	10	mobii	|- ( E* y [ y / x ] ph <-> E* y ps )
12	9 11	bitri	|- ( E* x ph <-> E* y ps )