Metamath Proof Explorer

Theorem ralbidar

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

Ref Expression
Hypotheses ralbidar.1 ⊢φ→∀x∈Aφ
ralbidar.2 ⊢φ∧x∈A→ψ↔χ
Assertion ralbidar ⊢φ→∀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.74d ⊢x∈A→x∈A→ψ↔χ→x∈A→ψ↔x∈A→χ
10 9 alimi ⊢∀xx∈A→x∈A→ψ↔χ→∀xx∈A→ψ↔x∈A→χ
11 albi ⊢∀xx∈A→ψ↔x∈A→χ→∀xx∈A→ψ↔∀xx∈A→χ
12 7 10 11 3syl ⊢φ→∀xx∈A→ψ↔∀xx∈A→χ
13 df-ral ⊢∀x∈Aψ↔∀xx∈A→ψ
14 df-ral ⊢∀x∈Aχ↔∀xx∈A→χ
15 12 13 14 3bitr4g ⊢φ→∀x∈Aψ↔∀x∈Aχ