Metamath Proof Explorer

Theorem axreplem

Description: Lemma for axrep2 and axrep3 . (Contributed by BJ, 6-Aug-2022)

Ref Expression
Assertion axreplem ⊢ x = y → ∃ u φ → ∀ v ψ ↔ ∃ w z ∈ x ∧ χ ↔ ∃ u φ → ∀ v ψ ↔ ∃ w z ∈ y ∧ χ

Proof

Step Hyp Ref Expression
1 elequ2 ⊢ x = y → z ∈ x ↔ z ∈ y
2 1 anbi1d ⊢ x = y → z ∈ x ∧ χ ↔ z ∈ y ∧ χ
3 2 exbidv ⊢ x = y → ∃ w z ∈ x ∧ χ ↔ ∃ w z ∈ y ∧ χ
4 3 bibi2d ⊢ x = y → ψ ↔ ∃ w z ∈ x ∧ χ ↔ ψ ↔ ∃ w z ∈ y ∧ χ
5 4 albidv ⊢ x = y → ∀ v ψ ↔ ∃ w z ∈ x ∧ χ ↔ ∀ v ψ ↔ ∃ w z ∈ y ∧ χ
6 5 imbi2d ⊢ x = y → φ → ∀ v ψ ↔ ∃ w z ∈ x ∧ χ ↔ φ → ∀ v ψ ↔ ∃ w z ∈ y ∧ χ
7 6 exbidv ⊢ x = y → ∃ u φ → ∀ v ψ ↔ ∃ w z ∈ x ∧ χ ↔ ∃ u φ → ∀ v ψ ↔ ∃ w z ∈ y ∧ χ