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

Proof

Step	Hyp	Ref	Expression
1		opelopabgf.x	$$⊢Ⅎx\psi$$
2		opelopabgf.y	$$⊢Ⅎy\chi$$
3		opelopabgf.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		opelopabgf.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
5		opelopabsb	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
7	6 1	nfsbcw	$$⊢Ⅎx\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi$$
8	3	sbcbidv	$$⊢x=A\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)$$
9	7 8	sbciegf	$$⊢A\in 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)$$
10	2 4	sbciegf	$$⊢B\in W\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
11	9 10	sylan9bb	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \chi \right)$$
12	5 11	bitrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \chi \right)$$