Metamath Proof Explorer

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	$⊢ (φ \land x = y) \to (ψ \leftrightarrow χ)$
	Assertion	opnneilem	$⊢ φ \to (\exists x \in J (S \subseteq x \land ψ) \leftrightarrow \exists y \in J (S \subseteq y \land χ))$

Step	Hyp	Ref	Expression
1		opnneilem.1	$⊢ (φ \land x = y) \to (ψ \leftrightarrow χ)$
2		sseq2	$⊢ x = y \to (S \subseteq x \leftrightarrow S \subseteq y)$
3	2	adantl	$⊢ (φ \land x = y) \to (S \subseteq x \leftrightarrow S \subseteq y)$
4	3 1	anbi12d	$⊢ (φ \land x = y) \to ((S \subseteq x \land ψ) \leftrightarrow (S \subseteq y \land χ))$
5	4	cbvrexdva	$⊢ φ \to (\exists x \in J (S \subseteq x \land ψ) \leftrightarrow \exists y \in J (S \subseteq y \land χ))$