Metamath Proof Explorer


Theorem elopabw

Description: Membership in a class abstraction of ordered pairs. Weaker version of elopab with a sethood antecedent, avoiding ax-sep , ax-nul , and ax-pr . Originally a subproof of elopab . (Contributed by SN, 11-Dec-2024)

Ref Expression
Assertion elopabw A V A x y | φ x y A = x y φ

Proof

Step Hyp Ref Expression
1 eqeq1 z = A z = x y A = x y
2 1 anbi1d z = A z = x y φ A = x y φ
3 2 2exbidv z = A x y z = x y φ x y A = x y φ
4 df-opab x y | φ = z | x y z = x y φ
5 3 4 elab2g A V A x y | φ x y A = x y φ