Metamath Proof Explorer

Theorem ceqsralt

Description: Restricted quantifier version of ceqsalt . (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 10-Oct-2016)

Ref Expression
Assertion ceqsralt ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x ∈ B x = A → φ ↔ ψ

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ x ∈ B x = A → φ ↔ ∀ x x ∈ B → x = A → φ
2 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
3 2 pm5.32ri ⊢ x ∈ B ∧ x = A ↔ A ∈ B ∧ x = A
4 3 imbi1i ⊢ x ∈ B ∧ x = A → φ ↔ A ∈ B ∧ x = A → φ
5 impexp ⊢ x ∈ B ∧ x = A → φ ↔ x ∈ B → x = A → φ
6 impexp ⊢ A ∈ B ∧ x = A → φ ↔ A ∈ B → x = A → φ
7 4 5 6 3bitr3i ⊢ x ∈ B → x = A → φ ↔ A ∈ B → x = A → φ
8 7 albii ⊢ ∀ x x ∈ B → x = A → φ ↔ ∀ x A ∈ B → x = A → φ
9 19.21v ⊢ ∀ x A ∈ B → x = A → φ ↔ A ∈ B → ∀ x x = A → φ
10 1 8 9 3bitri ⊢ ∀ x ∈ B x = A → φ ↔ A ∈ B → ∀ x x = A → φ
11 10 a1i ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x ∈ B x = A → φ ↔ A ∈ B → ∀ x x = A → φ
12 biimt ⊢ A ∈ B → ∀ x x = A → φ ↔ A ∈ B → ∀ x x = A → φ
13 12 3ad2ant3 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x x = A → φ ↔ A ∈ B → ∀ x x = A → φ
14 ceqsalt ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x x = A → φ ↔ ψ
15 11 13 14 3bitr2d ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x ∈ B x = A → φ ↔ ψ