Theorem cbvmow

Description: Rule used to change bound variables, using implicit substitution. Version of cbvmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 9-Mar-1995) (Revised by GG, 23-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvmow.1	|- F/ y ph
2		cbvmow.2	|- F/ x ps
3		cbvmow.3	|- ( x = y -> ( ph <-> ps ) )
4		nfv	|- F/ y x = z
5	1 4	nfim	|- F/ y ( ph -> x = z )
6		nfv	|- F/ x y = z
7	2 6	nfim	|- F/ x ( ps -> y = z )
8		equequ1	|- ( x = y -> ( x = z <-> y = z ) )
9	3 8	imbi12d	|- ( x = y -> ( ( ph -> x = z ) <-> ( ps -> y = z ) ) )
10	5 7 9	cbvalv1	|- ( A. x ( ph -> x = z ) <-> A. y ( ps -> y = z ) )
11	10	exbii	|- ( E. z A. x ( ph -> x = z ) <-> E. z A. y ( ps -> y = z ) )
12		df-mo	|- ( E* x ph <-> E. z A. x ( ph -> x = z ) )
13		df-mo	|- ( E* y ps <-> E. z A. y ( ps -> y = z ) )
14	11 12 13	3bitr4i	|- ( E* x ph <-> E* y ps )