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 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
Assertion opnneilem ( 𝜑 → ( ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) ↔ ∃ 𝑦𝐽 ( 𝑆𝑦𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 opnneilem.1 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
2 sseq2 ( 𝑥 = 𝑦 → ( 𝑆𝑥𝑆𝑦 ) )
3 2 adantl ( ( 𝜑𝑥 = 𝑦 ) → ( 𝑆𝑥𝑆𝑦 ) )
4 3 1 anbi12d ( ( 𝜑𝑥 = 𝑦 ) → ( ( 𝑆𝑥𝜓 ) ↔ ( 𝑆𝑦𝜒 ) ) )
5 4 cbvrexdva ( 𝜑 → ( ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) ↔ ∃ 𝑦𝐽 ( 𝑆𝑦𝜒 ) ) )