Metamath Proof Explorer


Theorem eqabbOLD

Description: Obsolete version of eqabb as of 12-Feb-2025. (Contributed by NM, 26-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion eqabbOLD A = x | φ x x A φ

Proof

Step Hyp Ref Expression
1 ax-5 y A x y A
2 hbab1 y x | φ x y x | φ
3 1 2 cleqh A = x | φ x x A x x | φ
4 abid x x | φ φ
5 4 bibi2i x A x x | φ x A φ
6 5 albii x x A x x | φ x x A φ
7 3 6 bitri A = x | φ x x A φ