Metamath Proof Explorer


Theorem eqopab2bw

Description: Equivalence of ordered pair abstraction equality and biconditional. Version of eqopab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 4-Jan-2017) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion eqopab2bw x y | φ = x y | ψ x y φ ψ

Proof

Step Hyp Ref Expression
1 ssopab2bw x y | φ x y | ψ x y φ ψ
2 ssopab2bw x y | ψ x y | φ x y ψ φ
3 1 2 anbi12i x y | φ x y | ψ x y | ψ x y | φ x y φ ψ x y ψ φ
4 eqss x y | φ = x y | ψ x y | φ x y | ψ x y | ψ x y | φ
5 2albiim x y φ ψ x y φ ψ x y ψ φ
6 3 4 5 3bitr4i x y | φ = x y | ψ x y φ ψ