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

Metamath Proof Explorer

Theorem opelopabgf

Description: The law of concretion. Theorem 9.5 of Quine p. 61. This version of opelopabg uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018)

Ref Expression
Hypotheses opelopabgf.x 
|- F/ x ps
opelopabgf.y 
|- F/ y ch
opelopabgf.1 
|- ( x = A -> ( ph <-> ps ) )
opelopabgf.2 
|- ( y = B -> ( ps <-> ch ) )
Assertion opelopabgf 
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )

Proof

Step Hyp Ref Expression
1 opelopabgf.x 
 |-  F/ x ps
2 opelopabgf.y 
 |-  F/ y ch
3 opelopabgf.1 
 |-  ( x = A -> ( ph <-> ps ) )
4 opelopabgf.2 
 |-  ( y = B -> ( ps <-> ch ) )
5 opelopabsb 
 |-  ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )
6 nfcv 
 |-  F/_ x B
7 6 1 nfsbcw 
 |-  F/ x [. B / y ]. ps
8 3 sbcbidv 
 |-  ( x = A -> ( [. B / y ]. ph <-> [. B / y ]. ps ) )
9 7 8 sbciegf 
 |-  ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. ps ) )
10 2 4 sbciegf 
 |-  ( B e. W -> ( [. B / y ]. ps <-> ch ) )
11 9 10 sylan9bb 
 |-  ( ( A e. V /\ B e. W ) -> ( [. A / x ]. [. B / y ]. ph <-> ch ) )
12 5 11 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )