Theorem cbvrmowOLD

Description: Obsolete version of cbvrmow as of 23-May-2024. (Contributed by NM, 16-Jun-2017) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrmowOLD.1	|- F/ y ph
2		cbvrmowOLD.2	|- F/ x ps
3		cbvrmowOLD.3	|- ( x = y -> ( ph <-> ps ) )
4	1 2 3	cbvrexw	|- ( E. x e. A ph <-> E. y e. A ps )
5	1 2 3	cbvreuw	|- ( 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 )