Theorem sbcop

Description: The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of each of its components. (Contributed by AV, 8-Apr-2023)

	Ref	Expression
Hypothesis	sbcop.z	$$⊢z=⟨x,y⟩\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	sbcop	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}⟨a,b⟩/z\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbcop.z	$$⊢z=⟨x,y⟩\to \left(\phi \leftrightarrow \psi \right)$$
2	1	sbcop1	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi$$
3	2	sbcbii	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi$$
4		sbcnestgw	$$⊢b\in \mathrm{V}\to \left(\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋b/y⦌⟨a,y⟩/z\underset{\dot{}}{]}\phi \right)$$
5	4	elv	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋b/y⦌⟨a,y⟩/z\underset{\dot{}}{]}\phi$$
6		csbopg	$$⊢b\in \mathrm{V}\to ⦋b/y⦌⟨a,y⟩=⟨⦋b/y⦌a,⦋b/y⦌y⟩$$
7	6	elv	$$⊢⦋b/y⦌⟨a,y⟩=⟨⦋b/y⦌a,⦋b/y⦌y⟩$$
8		vex	$$⊢b\in \mathrm{V}$$
9	8	csbconstgi	$$⊢⦋b/y⦌a=a$$
10	8	csbvargi	$$⊢⦋b/y⦌y=b$$
11	9 10	opeq12i	$$⊢⟨⦋b/y⦌a,⦋b/y⦌y⟩=⟨a,b⟩$$
12	7 11	eqtri	$$⊢⦋b/y⦌⟨a,y⟩=⟨a,b⟩$$
13		dfsbcq	$$⊢⦋b/y⦌⟨a,y⟩=⟨a,b⟩\to \left(\underset{\dot{}}{[}⦋b/y⦌⟨a,y⟩/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨a,b⟩/z\underset{\dot{}}{]}\phi \right)$$
14	12 13	ax-mp	$$⊢\underset{\dot{}}{[}⦋b/y⦌⟨a,y⟩/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨a,b⟩/z\underset{\dot{}}{]}\phi$$
15	3 5 14	3bitri	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}⟨a,b⟩/z\underset{\dot{}}{]}\phi$$