Description: The law of concretion. Theorem 9.5 of Quine p. 61. (Contributed by Mario Carneiro, 19-Dec-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opelopaba.1 | |- A e. _V |
|
opelopaba.2 | |- B e. _V |
||
opelopaba.3 | |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
||
Assertion | opelopaba | |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelopaba.1 | |- A e. _V |
|
2 | opelopaba.2 | |- B e. _V |
|
3 | opelopaba.3 | |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
|
4 | 3 | opelopabga | |- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) ) |
5 | 1 2 4 | mp2an | |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) |