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 )