This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelopabf

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 NM, 19-Dec-2008)

Ref Expression
Hypotheses opelopabf.x 
|- F/ x ps
opelopabf.y 
|- F/ y ch
opelopabf.1 
|- A e. _V
opelopabf.2 
|- B e. _V
opelopabf.3 
|- ( x = A -> ( ph <-> ps ) )
opelopabf.4 
|- ( y = B -> ( ps <-> ch ) )
Assertion opelopabf 
|- ( <. A , B >. e. { <. x , y >. | ph } <-> ch )

Proof

Step Hyp Ref Expression
1 opelopabf.x 
 |-  F/ x ps
2 opelopabf.y 
 |-  F/ y ch
3 opelopabf.1 
 |-  A e. _V
4 opelopabf.2 
 |-  B e. _V
5 opelopabf.3 
 |-  ( x = A -> ( ph <-> ps ) )
6 opelopabf.4 
 |-  ( y = B -> ( ps <-> ch ) )
7 opelopabsb 
 |-  ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )
8 nfcv 
 |-  F/_ x B
9 8 1 nfsbcw 
 |-  F/ x [. B / y ]. ps
10 5 sbcbidv 
 |-  ( x = A -> ( [. B / y ]. ph <-> [. B / y ]. ps ) )
11 9 10 sbciegf 
 |-  ( A e. _V -> ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. ps ) )
12 3 11 ax-mp 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. ps )
13 2 6 sbciegf 
 |-  ( B e. _V -> ( [. B / y ]. ps <-> ch ) )
14 4 13 ax-mp 
 |-  ( [. B / y ]. ps <-> ch )
15 7 12 14 3bitri 
 |-  ( <. A , B >. e. { <. x , y >. | ph } <-> ch )