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	$$⊢Ⅎx\psi$$
	opelopabf.y	$$⊢Ⅎy\chi$$
	opelopabf.1	$$⊢A\in \mathrm{V}$$
	opelopabf.2	$$⊢B\in \mathrm{V}$$
	opelopabf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	opelopabf.4	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	opelopabf	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \chi$$

Proof

Step	Hyp	Ref	Expression
1		opelopabf.x	$$⊢Ⅎx\psi$$
2		opelopabf.y	$$⊢Ⅎy\chi$$
3		opelopabf.1	$$⊢A\in \mathrm{V}$$
4		opelopabf.2	$$⊢B\in \mathrm{V}$$
5		opelopabf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
6		opelopabf.4	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
7		opelopabsb	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
9	8 1	nfsbcw	$$⊢Ⅎx\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi$$
10	5	sbcbidv	$$⊢x=A\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)$$
11	9 10	sbciegf	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)$$
12	3 11	ax-mp	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi$$
13	2 6	sbciegf	$$⊢B\in \mathrm{V}\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
14	4 13	ax-mp	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi$$
15	7 12 14	3bitri	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \chi$$