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 ) )