Theorem sbcop1

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

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

Proof

Step	Hyp	Ref	Expression
1		sbcop.z	$$⊢z=⟨x,y⟩\to \left(\phi \leftrightarrow \psi \right)$$
2		sbc5	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \exists x\left(x=a\wedge \psi \right)$$
3		opeq1	$$⊢a=x\to ⟨a,y⟩=⟨x,y⟩$$
4	3	equcoms	$$⊢x=a\to ⟨a,y⟩=⟨x,y⟩$$
5	4	eqeq2d	$$⊢x=a\to \left(z=⟨a,y⟩\leftrightarrow z=⟨x,y⟩\right)$$
6	1	biimprd	$$⊢z=⟨x,y⟩\to \left(\psi \to \phi \right)$$
7	5 6	syl6bi	$$⊢x=a\to \left(z=⟨a,y⟩\to \left(\psi \to \phi \right)\right)$$
8	7	com23	$$⊢x=a\to \left(\psi \to \left(z=⟨a,y⟩\to \phi \right)\right)$$
9	8	imp	$$⊢\left(x=a\wedge \psi \right)\to \left(z=⟨a,y⟩\to \phi \right)$$
10	9	exlimiv	$$⊢\exists x\left(x=a\wedge \psi \right)\to \left(z=⟨a,y⟩\to \phi \right)$$
11	2 10	sylbi	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \left(z=⟨a,y⟩\to \phi \right)$$
12	11	alrimiv	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \forall z\left(z=⟨a,y⟩\to \phi \right)$$
13		opex	$$⊢⟨a,y⟩\in \mathrm{V}$$
14	13	sbc6	$$⊢\underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi \leftrightarrow \forall z\left(z=⟨a,y⟩\to \phi \right)$$
15	12 14	sylibr	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi$$
16		sbc5	$$⊢\underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi \leftrightarrow \exists z\left(z=⟨a,y⟩\wedge \phi \right)$$
17	1	biimpd	$$⊢z=⟨x,y⟩\to \left(\phi \to \psi \right)$$
18	5 17	syl6bi	$$⊢x=a\to \left(z=⟨a,y⟩\to \left(\phi \to \psi \right)\right)$$
19	18	com3l	$$⊢z=⟨a,y⟩\to \left(\phi \to \left(x=a\to \psi \right)\right)$$
20	19	imp	$$⊢\left(z=⟨a,y⟩\wedge \phi \right)\to \left(x=a\to \psi \right)$$
21	20	alrimiv	$$⊢\left(z=⟨a,y⟩\wedge \phi \right)\to \forall x\left(x=a\to \psi \right)$$
22		vex	$$⊢a\in \mathrm{V}$$
23	22	sbc6	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \forall x\left(x=a\to \psi \right)$$
24	21 23	sylibr	$$⊢\left(z=⟨a,y⟩\wedge \phi \right)\to \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$
25	24	exlimiv	$$⊢\exists z\left(z=⟨a,y⟩\wedge \phi \right)\to \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$
26	16 25	sylbi	$$⊢\underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$
27	15 26	impbii	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}⟨a,y⟩/z\underset{\dot{}}{]}\phi$$