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ψ↔∃wz∈x∧χ↔∃uφ→∀vψ↔∃wz∈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→∃wz∈x∧χ↔∃wz∈y∧χ
4 3 bibi2d ⊢x=y→ψ↔∃wz∈x∧χ↔ψ↔∃wz∈y∧χ
5 4 albidv ⊢x=y→∀vψ↔∃wz∈x∧χ↔∀vψ↔∃wz∈y∧χ
6 5 imbi2d ⊢x=y→φ→∀vψ↔∃wz∈x∧χ↔φ→∀vψ↔∃wz∈y∧χ
7 6 exbidv ⊢x=y→∃uφ→∀vψ↔∃wz∈x∧χ↔∃uφ→∀vψ↔∃wz∈y∧χ