Metamath Proof Explorer


Theorem 2rexbidv

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006)

Ref Expression
Hypothesis 2rexbidv.1 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion 2rexbidv ( 𝜑 → ( ∃ 𝑥𝐴𝑦𝐵 𝜓 ↔ ∃ 𝑥𝐴𝑦𝐵 𝜒 ) )

Proof

Step Hyp Ref Expression
1 2rexbidv.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 1 rexbidv ( 𝜑 → ( ∃ 𝑦𝐵 𝜓 ↔ ∃ 𝑦𝐵 𝜒 ) )
3 2 rexbidv ( 𝜑 → ( ∃ 𝑥𝐴𝑦𝐵 𝜓 ↔ ∃ 𝑥𝐴𝑦𝐵 𝜒 ) )