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 e. V -> ( A e. { <. x , y >. | ph } <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1
 |-  ( z = A -> ( z = <. x , y >. <-> A = <. x , y >. ) )
2 1 anbi1d
 |-  ( z = A -> ( ( z = <. x , y >. /\ ph ) <-> ( A = <. x , y >. /\ ph ) ) )
3 2 2exbidv
 |-  ( z = A -> ( E. x E. y ( z = <. x , y >. /\ ph ) <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )
4 df-opab
 |-  { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
5 3 4 elab2g
 |-  ( A e. V -> ( A e. { <. x , y >. | ph } <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )