Theorem cbvrmo

Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrmow when possible. (Contributed by NM, 16-Jun-2017) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvral.1	|- F/ y ph
2		cbvral.2	|- F/ x ps
3		cbvral.3	|- ( x = y -> ( ph <-> ps ) )
4	1 2 3	cbvrex	|- ( E. x e. A ph <-> E. y e. A ps )
5	1 2 3	cbvreu	|- ( E! x e. A ph <-> E! y e. A ps )
6	4 5	imbi12i	|- ( ( E. x e. A ph -> E! x e. A ph ) <-> ( E. y e. A ps -> E! y e. A ps ) )
7		rmo5	|- ( E* x e. A ph <-> ( E. x e. A ph -> E! x e. A ph ) )
8		rmo5	|- ( E* y e. A ps <-> ( E. y e. A ps -> E! y e. A ps ) )
9	6 7 8	3bitr4i	|- ( E* x e. A ph <-> E* y e. A ps )