This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reximd2a

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Hypotheses reximd2a.1 ⊢ Ⅎ 𝑥 𝜑
reximd2a.2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝑥 ∈ 𝐵 )
reximd2a.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
reximd2a.4 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
Assertion reximd2a ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜒 )

Proof

Step Hyp Ref Expression
1 reximd2a.1 ⊢ Ⅎ 𝑥 𝜑
2 reximd2a.2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝑥 ∈ 𝐵 )
3 reximd2a.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
4 reximd2a.4 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
5 2 3 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) )
6 5 expl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) )
7 1 6 eximd ⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) )
8 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
9 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 𝜒 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) )
10 7 8 9 3imtr4g ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐵 𝜒 ) )
11 4 10 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜒 )