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

Metamath Proof Explorer

Theorem eqabbw

Description: Version of eqabb using implicit substitution, which requires fewer axioms. (Contributed by GG and AV, 18-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 eqabbw.1 ⊢ x = y → φ ↔ ψ
2 dfcleq ⊢ A = x | φ ↔ ∀ y y ∈ A ↔ y ∈ x | φ
3 df-clab ⊢ y ∈ x | φ ↔ y x φ
4 1 sbievw ⊢ y x φ ↔ ψ
5 3 4 bitri ⊢ y ∈ x | φ ↔ ψ
6 5 bibi2i ⊢ y ∈ A ↔ y ∈ x | φ ↔ y ∈ A ↔ ψ
7 6 albii ⊢ ∀ y y ∈ A ↔ y ∈ x | φ ↔ ∀ y y ∈ A ↔ ψ
8 2 7 bitri ⊢ A = x | φ ↔ ∀ y y ∈ A ↔ ψ