Metamath Proof Explorer


Theorem opelopabaf

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 )

Proof

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 )