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	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜒 )