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ψ∧∀xx=A→φ↔ψ∧A∈B→∀x∈Bx=A→φ↔ψ

Proof

Step Hyp Ref Expression
1 biimt ⊢A∈B→∀xx=A→φ↔A∈B→∀xx=A→φ
2 df-ral ⊢∀x∈Bx=A→φ↔∀xx∈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 ⊢∀xx∈B→x=A→φ↔∀xA∈B→x=A→φ
10 19.21v ⊢∀xA∈B→x=A→φ↔A∈B→∀xx=A→φ
11 2 9 10 3bitrri ⊢A∈B→∀xx=A→φ↔∀x∈Bx=A→φ
12 1 11 bitrdi ⊢A∈B→∀xx=A→φ↔∀x∈Bx=A→φ
13 12 3ad2ant3 ⊢Ⅎxψ∧∀xx=A→φ↔ψ∧A∈B→∀xx=A→φ↔∀x∈Bx=A→φ
14 ceqsalt ⊢Ⅎxψ∧∀xx=A→φ↔ψ∧A∈B→∀xx=A→φ↔ψ
15 13 14 bitr3d ⊢Ⅎxψ∧∀xx=A→φ↔ψ∧A∈B→∀x∈Bx=A→φ↔ψ