Metamath Proof Explorer


Theorem sepnsepolem1

Description: Lemma for sepnsepo . (Contributed by Zhi Wang, 1-Sep-2024)

Ref Expression
Assertion sepnsepolem1 ( ∃ 𝑥𝐽𝑦𝐽 ( 𝜑𝜓𝜒 ) ↔ ∃ 𝑥𝐽 ( 𝜑 ∧ ∃ 𝑦𝐽 ( 𝜓𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 3anass ( ( 𝜑𝜓𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓𝜒 ) ) )
2 1 2rexbii ( ∃ 𝑥𝐽𝑦𝐽 ( 𝜑𝜓𝜒 ) ↔ ∃ 𝑥𝐽𝑦𝐽 ( 𝜑 ∧ ( 𝜓𝜒 ) ) )
3 r19.42v ( ∃ 𝑦𝐽 ( 𝜑 ∧ ( 𝜓𝜒 ) ) ↔ ( 𝜑 ∧ ∃ 𝑦𝐽 ( 𝜓𝜒 ) ) )
4 3 rexbii ( ∃ 𝑥𝐽𝑦𝐽 ( 𝜑 ∧ ( 𝜓𝜒 ) ) ↔ ∃ 𝑥𝐽 ( 𝜑 ∧ ∃ 𝑦𝐽 ( 𝜓𝜒 ) ) )
5 2 4 bitri ( ∃ 𝑥𝐽𝑦𝐽 ( 𝜑𝜓𝜒 ) ↔ ∃ 𝑥𝐽 ( 𝜑 ∧ ∃ 𝑦𝐽 ( 𝜓𝜒 ) ) )