Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Version of opabid with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Apr-1995) Avoid ax-13 . (Revised by GG, 26-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | opabidw | |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opex | |- <. x , y >. e. _V |
|
| 2 | copsexgw | |- ( z = <. x , y >. -> ( ph <-> E. x E. y ( z = <. x , y >. /\ ph ) ) ) |
|
| 3 | 2 | bicomd | |- ( z = <. x , y >. -> ( E. x E. y ( z = <. x , y >. /\ ph ) <-> ph ) ) |
| 4 | df-opab | |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) } |
|
| 5 | 1 3 4 | elab2 | |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) |