Metamath Proof Explorer

Theorem rexbidar

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

Ref Expression
Hypotheses ralbidar.1 ⊢ φ → ∀ x ∈ A φ
ralbidar.2 ⊢ φ ∧ x ∈ A → ψ ↔ χ
Assertion rexbidar ⊢ φ → ∃ x ∈ A ψ ↔ ∃ x ∈ A χ

Proof

Step Hyp Ref Expression
1 ralbidar.1 ⊢ φ → ∀ x ∈ A φ
2 ralbidar.2 ⊢ φ ∧ x ∈ A → ψ ↔ χ
3 2 ex ⊢ φ → x ∈ A → ψ ↔ χ
4 3 ralimi ⊢ ∀ x ∈ A φ → ∀ x ∈ A x ∈ A → ψ ↔ χ
5 1 4 syl ⊢ φ → ∀ x ∈ A x ∈ A → ψ ↔ χ
6 df-ral ⊢ ∀ x ∈ A x ∈ A → ψ ↔ χ ↔ ∀ x x ∈ A → x ∈ A → ψ ↔ χ
7 5 6 sylib ⊢ φ → ∀ x x ∈ A → x ∈ A → ψ ↔ χ
8 pm2.43 ⊢ x ∈ A → x ∈ A → ψ ↔ χ → x ∈ A → ψ ↔ χ
9 8 pm5.32d ⊢ x ∈ A → x ∈ A → ψ ↔ χ → x ∈ A ∧ ψ ↔ x ∈ A ∧ χ
10 9 alimi ⊢ ∀ x x ∈ A → x ∈ A → ψ ↔ χ → ∀ x x ∈ A ∧ ψ ↔ x ∈ A ∧ χ
11 exbi ⊢ ∀ x x ∈ A ∧ ψ ↔ x ∈ A ∧ χ → ∃ x x ∈ A ∧ ψ ↔ ∃ x x ∈ A ∧ χ
12 7 10 11 3syl ⊢ φ → ∃ x x ∈ A ∧ ψ ↔ ∃ x x ∈ A ∧ χ
13 df-rex ⊢ ∃ x ∈ A ψ ↔ ∃ x x ∈ A ∧ ψ
14 df-rex ⊢ ∃ x ∈ A χ ↔ ∃ x x ∈ A ∧ χ
15 12 13 14 3bitr4g ⊢ φ → ∃ x ∈ A ψ ↔ ∃ x ∈ A χ