Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker opabidw when possible. (Contributed by NM, 14-Apr-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | opabid | |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opex | |- <. x , y >. e. _V |
|
| 2 | copsexg | |- ( 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 ) |