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 biimt ⊢ A ∈ B → ∀ x x = A → φ ↔ A ∈ B → ∀ x x = A → φ
2 df-ral ⊢ ∀ x ∈ B x = A → φ ↔ ∀ x x ∈ B → x = A → φ
3 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
4 3 pm5.32ri ⊢ x ∈ B ∧ x = A ↔ A ∈ B ∧ x = A
5 4 imbi1i ⊢ x ∈ B ∧ x = A → φ ↔ A ∈ B ∧ x = A → φ
6 impexp ⊢ x ∈ B ∧ x = A → φ ↔ x ∈ B → x = A → φ
7 impexp ⊢ A ∈ B ∧ x = A → φ ↔ A ∈ B → x = A → φ
8 5 6 7 3bitr3i ⊢ x ∈ B → x = A → φ ↔ A ∈ B → x = A → φ
9 8 albii ⊢ ∀ x x ∈ B → x = A → φ ↔ ∀ x A ∈ B → x = A → φ
10 19.21v ⊢ ∀ x A ∈ B → x = A → φ ↔ A ∈ B → ∀ x x = A → φ
11 2 9 10 3bitrri ⊢ A ∈ B → ∀ x x = A → φ ↔ ∀ x ∈ B x = A → φ
12 1 11 bitrdi ⊢ A ∈ B → ∀ x x = A → φ ↔ ∀ x ∈ B x = A → φ
13 12 3ad2ant3 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x x = A → φ ↔ ∀ x ∈ B x = A → φ
14 ceqsalt ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x x = A → φ ↔ ψ
15 13 14 bitr3d ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x ∈ B x = A → φ ↔ ψ