This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqabcbw

Description: Version of eqabcb using implicit substitution, which requires fewer axioms. (Contributed by TM, 24-Jan-2026)

Ref Expression
Hypothesis eqabbw.1 ⊢ x = y → φ ↔ ψ
Assertion eqabcbw ⊢ x | φ = A ↔ ∀ y ψ ↔ y ∈ A

Proof

Step Hyp Ref Expression
1 eqabbw.1 ⊢ x = y → φ ↔ ψ
2 1 eqabbw ⊢ A = x | φ ↔ ∀ y y ∈ A ↔ ψ
3 eqcom ⊢ x | φ = A ↔ A = x | φ
4 bicom ⊢ ψ ↔ y ∈ A ↔ y ∈ A ↔ ψ
5 4 albii ⊢ ∀ y ψ ↔ y ∈ A ↔ ∀ y y ∈ A ↔ ψ
6 2 3 5 3bitr4i ⊢ x | φ = A ↔ ∀ y ψ ↔ y ∈ A