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