Metamath Proof Explorer


Theorem opelopaba

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 )

Proof

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 )