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∈Ax∈A→ψ↔χ
5 1 4 syl ⊢φ→∀x∈Ax∈A→ψ↔χ
6 df-ral ⊢∀x∈Ax∈A→ψ↔χ↔∀xx∈A→x∈A→ψ↔χ
7 5 6 sylib ⊢φ→∀xx∈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 ⊢∀xx∈A→x∈A→ψ↔χ→∀xx∈A∧ψ↔x∈A∧χ
11 exbi ⊢∀xx∈A∧ψ↔x∈A∧χ→∃xx∈A∧ψ↔∃xx∈A∧χ
12 7 10 11 3syl ⊢φ→∃xx∈A∧ψ↔∃xx∈A∧χ
13 df-rex ⊢∃x∈Aψ↔∃xx∈A∧ψ
14 df-rex ⊢∃x∈Aχ↔∃xx∈A∧χ
15 12 13 14 3bitr4g ⊢φ→∃x∈Aψ↔∃x∈Aχ