Theorem rexbidar

Description: More general form of rexbida . (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Hypotheses	ralbidar.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 )
	ralbidar.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	rexbidar	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralbidar.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 )
2		ralbidar.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
3	2	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
4	3	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
5	1 4	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) )
7	5 6	sylib	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) )
8		pm2.43	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
9	8	pm5.32d	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
10	9	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
11		exbi	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
12	7 10 11	3syl	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
13		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
14		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜒 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) )
15	12 13 14	3bitr4g	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 𝜒 ) )