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 ∈ 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.74d ⊢ x ∈ A → x ∈ A → ψ ↔ χ → x ∈ A → ψ ↔ x ∈ A → χ
10 9 alimi ⊢ ∀ x x ∈ A → x ∈ A → ψ ↔ χ → ∀ x x ∈ A → ψ ↔ x ∈ A → χ
11 albi ⊢ ∀ x x ∈ A → ψ ↔ x ∈ A → χ → ∀ x x ∈ A → ψ ↔ ∀ x x ∈ A → χ
12 7 10 11 3syl ⊢ φ → ∀ x x ∈ A → ψ ↔ ∀ x x ∈ A → χ
13 df-ral ⊢ ∀ x ∈ A ψ ↔ ∀ x x ∈ A → ψ
14 df-ral ⊢ ∀ x ∈ A χ ↔ ∀ x x ∈ A → χ
15 12 13 14 3bitr4g ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ A χ