Theorem opsbc2ie

Description: Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		opsbc2ie.a	$$⊢p=⟨a,b⟩\to \left(\phi \leftrightarrow \chi \right)$$
2	1	sbcth	$$⊢x\in \mathrm{V}\to \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\left(p=⟨a,b⟩\to \left(\phi \leftrightarrow \chi \right)\right)$$
3		sbcim1	$$⊢\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\left(p=⟨a,b⟩\to \left(\phi \leftrightarrow \chi \right)\right)\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}p=⟨a,b⟩\to \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\left(\phi \leftrightarrow \chi \right)\right)$$
4	2 3	syl	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}p=⟨a,b⟩\to \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\left(\phi \leftrightarrow \chi \right)\right)$$
5		sbceq2g	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}p=⟨a,b⟩\leftrightarrow p=⦋x/a⦌⟨a,b⟩\right)$$
6		csbopg	$$⊢x\in \mathrm{V}\to ⦋x/a⦌⟨a,b⟩=⟨⦋x/a⦌a,⦋x/a⦌b⟩$$
7		csbvarg	$$⊢x\in \mathrm{V}\to ⦋x/a⦌a=x$$
8		csbconstg	$$⊢x\in \mathrm{V}\to ⦋x/a⦌b=b$$
9	7 8	opeq12d	$$⊢x\in \mathrm{V}\to ⟨⦋x/a⦌a,⦋x/a⦌b⟩=⟨x,b⟩$$
10	6 9	eqtrd	$$⊢x\in \mathrm{V}\to ⦋x/a⦌⟨a,b⟩=⟨x,b⟩$$
11	10	eqeq2d	$$⊢x\in \mathrm{V}\to \left(p=⦋x/a⦌⟨a,b⟩\leftrightarrow p=⟨x,b⟩\right)$$
12	5 11	bitrd	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}p=⟨a,b⟩\leftrightarrow p=⟨x,b⟩\right)$$
13		sbcbig	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\left(\phi \leftrightarrow \chi \right)\leftrightarrow \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
14		sbcg	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
15	14	bibi1d	$$⊢x\in \mathrm{V}\to \left(\left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
16	13 15	bitrd	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\left(\phi \leftrightarrow \chi \right)\leftrightarrow \left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
17	4 12 16	3imtr3d	$$⊢x\in \mathrm{V}\to \left(p=⟨x,b⟩\to \left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
18	17	elv	$$⊢p=⟨x,b⟩\to \left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)$$
19	18	sbcth	$$⊢y\in \mathrm{V}\to \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\left(p=⟨x,b⟩\to \left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
20		sbcim1	$$⊢\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\left(p=⟨x,b⟩\to \left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}p=⟨x,b⟩\to \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
21	19 20	syl	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}p=⟨x,b⟩\to \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
22		sbceq2g	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}p=⟨x,b⟩\leftrightarrow p=⦋y/b⦌⟨x,b⟩\right)$$
23		csbopg	$$⊢y\in \mathrm{V}\to ⦋y/b⦌⟨x,b⟩=⟨⦋y/b⦌x,⦋y/b⦌b⟩$$
24		csbconstg	$$⊢y\in \mathrm{V}\to ⦋y/b⦌x=x$$
25		csbvarg	$$⊢y\in \mathrm{V}\to ⦋y/b⦌b=y$$
26	24 25	opeq12d	$$⊢y\in \mathrm{V}\to ⟨⦋y/b⦌x,⦋y/b⦌b⟩=⟨x,y⟩$$
27	23 26	eqtrd	$$⊢y\in \mathrm{V}\to ⦋y/b⦌⟨x,b⟩=⟨x,y⟩$$
28	27	eqeq2d	$$⊢y\in \mathrm{V}\to \left(p=⦋y/b⦌⟨x,b⟩\leftrightarrow p=⟨x,y⟩\right)$$
29	22 28	bitrd	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}p=⟨x,b⟩\leftrightarrow p=⟨x,y⟩\right)$$
30		sbcbig	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
31		sbcg	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
32	31	bibi1d	$$⊢y\in \mathrm{V}\to \left(\left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
33	30 32	bitrd	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
34	21 29 33	3imtr3d	$$⊢y\in \mathrm{V}\to \left(p=⟨x,y⟩\to \left(\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)\right)$$
35	34	elv	$$⊢p=⟨x,y⟩\to \left(\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\chi \right)$$