Theorem sbcpr

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

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

Proof

Step	Hyp	Ref	Expression
1		sbcpr.x	$$⊢p=\left\{x,y\right\}\to \left(\phi \leftrightarrow \psi \right)$$
2		sbc5	$$⊢\underset{\dot{}}{[}\left\{a,b\right\}/p\underset{\dot{}}{]}\phi \leftrightarrow \exists p\left(p=\left\{a,b\right\}\wedge \phi \right)$$
3		preq12	$$⊢\left(x=a\wedge y=b\right)\to \left\{x,y\right\}=\left\{a,b\right\}$$
4	3	eqcomd	$$⊢\left(x=a\wedge y=b\right)\to \left\{a,b\right\}=\left\{x,y\right\}$$
5	4	eqeq2d	$$⊢\left(x=a\wedge y=b\right)\to \left(p=\left\{a,b\right\}\leftrightarrow p=\left\{x,y\right\}\right)$$
6	5	biimpa	$$⊢\left(\left(x=a\wedge y=b\right)\wedge p=\left\{a,b\right\}\right)\to p=\left\{x,y\right\}$$
7	6 1	syl	$$⊢\left(\left(x=a\wedge y=b\right)\wedge p=\left\{a,b\right\}\right)\to \left(\phi \leftrightarrow \psi \right)$$
8	7	biimpd	$$⊢\left(\left(x=a\wedge y=b\right)\wedge p=\left\{a,b\right\}\right)\to \left(\phi \to \psi \right)$$
9	8	expcom	$$⊢p=\left\{a,b\right\}\to \left(\left(x=a\wedge y=b\right)\to \left(\phi \to \psi \right)\right)$$
10	9	expd	$$⊢p=\left\{a,b\right\}\to \left(x=a\to \left(y=b\to \left(\phi \to \psi \right)\right)\right)$$
11	10	com24	$$⊢p=\left\{a,b\right\}\to \left(\phi \to \left(y=b\to \left(x=a\to \psi \right)\right)\right)$$
12	11	imp31	$$⊢\left(\left(p=\left\{a,b\right\}\wedge \phi \right)\wedge y=b\right)\to \left(x=a\to \psi \right)$$
13	12	alrimiv	$$⊢\left(\left(p=\left\{a,b\right\}\wedge \phi \right)\wedge y=b\right)\to \forall x\left(x=a\to \psi \right)$$
14		vex	$$⊢a\in \mathrm{V}$$
15	14	sbc6	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \forall x\left(x=a\to \psi \right)$$
16	13 15	sylibr	$$⊢\left(\left(p=\left\{a,b\right\}\wedge \phi \right)\wedge y=b\right)\to \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$
17	16	ex	$$⊢\left(p=\left\{a,b\right\}\wedge \phi \right)\to \left(y=b\to \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)$$
18	17	alrimiv	$$⊢\left(p=\left\{a,b\right\}\wedge \phi \right)\to \forall y\left(y=b\to \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)$$
19		vex	$$⊢b\in \mathrm{V}$$
20	19	sbc6	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \forall y\left(y=b\to \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)$$
21	18 20	sylibr	$$⊢\left(p=\left\{a,b\right\}\wedge \phi \right)\to \underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$
22	21	exlimiv	$$⊢\exists p\left(p=\left\{a,b\right\}\wedge \phi \right)\to \underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$
23	2 22	sylbi	$$⊢\underset{\dot{}}{[}\left\{a,b\right\}/p\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$
24		sbc5	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \exists y\left(y=b\wedge \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)$$
25		sbc5	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \exists x\left(x=a\wedge \psi \right)$$
26	1	bicomd	$$⊢p=\left\{x,y\right\}\to \left(\psi \leftrightarrow \phi \right)$$
27	6 26	syl	$$⊢\left(\left(x=a\wedge y=b\right)\wedge p=\left\{a,b\right\}\right)\to \left(\psi \leftrightarrow \phi \right)$$
28	27	biimpd	$$⊢\left(\left(x=a\wedge y=b\right)\wedge p=\left\{a,b\right\}\right)\to \left(\psi \to \phi \right)$$
29	28	expcom	$$⊢p=\left\{a,b\right\}\to \left(\left(x=a\wedge y=b\right)\to \left(\psi \to \phi \right)\right)$$
30	29	com13	$$⊢\psi \to \left(\left(x=a\wedge y=b\right)\to \left(p=\left\{a,b\right\}\to \phi \right)\right)$$
31	30	expd	$$⊢\psi \to \left(x=a\to \left(y=b\to \left(p=\left\{a,b\right\}\to \phi \right)\right)\right)$$
32	31	impcom	$$⊢\left(x=a\wedge \psi \right)\to \left(y=b\to \left(p=\left\{a,b\right\}\to \phi \right)\right)$$
33	32	exlimiv	$$⊢\exists x\left(x=a\wedge \psi \right)\to \left(y=b\to \left(p=\left\{a,b\right\}\to \phi \right)\right)$$
34	25 33	sylbi	$$⊢\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \left(y=b\to \left(p=\left\{a,b\right\}\to \phi \right)\right)$$
35	34	impcom	$$⊢\left(y=b\wedge \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)\to \left(p=\left\{a,b\right\}\to \phi \right)$$
36	35	exlimiv	$$⊢\exists y\left(y=b\wedge \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)\to \left(p=\left\{a,b\right\}\to \phi \right)$$
37	24 36	sylbi	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \left(p=\left\{a,b\right\}\to \phi \right)$$
38	37	alrimiv	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \forall p\left(p=\left\{a,b\right\}\to \phi \right)$$
39		prex	$$⊢\left\{a,b\right\}\in \mathrm{V}$$
40	39	sbc6	$$⊢\underset{\dot{}}{[}\left\{a,b\right\}/p\underset{\dot{}}{]}\phi \leftrightarrow \forall p\left(p=\left\{a,b\right\}\to \phi \right)$$
41	38 40	sylibr	$$⊢\underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left\{a,b\right\}/p\underset{\dot{}}{]}\phi$$
42	23 41	impbii	$$⊢\underset{\dot{}}{[}\left\{a,b\right\}/p\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/y\underset{\dot{}}{]}\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi$$