Theorem opnneilem

Description: Lemma factoring out common proof steps of opnneil and opnneirv . (Contributed by Zhi Wang, 31-Aug-2024)

	Ref	Expression
Hypothesis	opnneilem.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	opnneilem	|- ( ph -> ( E. x e. J ( S C_ x /\ ps ) <-> E. y e. J ( S C_ y /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		opnneilem.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2		sseq2	|- ( x = y -> ( S C_ x <-> S C_ y ) )
3	2	adantl	|- ( ( ph /\ x = y ) -> ( S C_ x <-> S C_ y ) )
4	3 1	anbi12d	|- ( ( ph /\ x = y ) -> ( ( S C_ x /\ ps ) <-> ( S C_ y /\ ch ) ) )
5	4	cbvrexdva	|- ( ph -> ( E. x e. J ( S C_ x /\ ps ) <-> E. y e. J ( S C_ y /\ ch ) ) )