Description: The law of concretion. Theorem 9.5 of Quine p. 61. This version of opelopab uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013) (Proof shortened by Mario Carneiro, 18-Nov-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opelopabaf.x | |- F/ x ps |
|
opelopabaf.y | |- F/ y ps |
||
opelopabaf.1 | |- A e. _V |
||
opelopabaf.2 | |- B e. _V |
||
opelopabaf.3 | |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
||
Assertion | opelopabaf | |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelopabaf.x | |- F/ x ps |
|
2 | opelopabaf.y | |- F/ y ps |
|
3 | opelopabaf.1 | |- A e. _V |
|
4 | opelopabaf.2 | |- B e. _V |
|
5 | opelopabaf.3 | |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
|
6 | opelopabsb | |- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) |
|
7 | nfv | |- F/ x B e. _V |
|
8 | 1 2 7 5 | sbc2iegf | |- ( ( A e. _V /\ B e. _V ) -> ( [. A / x ]. [. B / y ]. ph <-> ps ) ) |
9 | 3 4 8 | mp2an | |- ( [. A / x ]. [. B / y ]. ph <-> ps ) |
10 | 6 9 | bitri | |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) |