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 | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opnneilem.1 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | |
2 | sseq2 | ⊢ ( 𝑥 = 𝑦 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑦 ) ) | |
3 | 2 | adantl | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑦 ) ) |
4 | 3 1 | anbi12d | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ↔ ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) ) |
5 | 4 | cbvrexdva | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) ) |