Theorem cbvrmow

Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 16-Jun-2017) (Revised by Gino Giotto, 23-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrmow.1	|- F/ y ph
2		cbvrmow.2	|- F/ x ps
3		cbvrmow.3	|- ( x = y -> ( ph <-> ps ) )
4		nfv	|- F/ y x e. A
5	4 1	nfan	|- F/ y ( x e. A /\ ph )
6		nfv	|- F/ x y e. A
7	6 2	nfan	|- F/ x ( y e. A /\ ps )
8		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
9	8 3	anbi12d	|- ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
10	5 7 9	cbvmow	|- ( E* x ( x e. A /\ ph ) <-> E* y ( y e. A /\ ps ) )
11		df-rmo	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
12		df-rmo	|- ( E* y e. A ps <-> E* y ( y e. A /\ ps ) )
13	10 11 12	3bitr4i	|- ( E* x e. A ph <-> E* y e. A ps )