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 ) ) ) |
| 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 ) ) ) |