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	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 ↔ 𝜒 ) )
Assertion	opsbc2ie	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		opsbc2ie.a	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 ↔ 𝜒 ) )
2	1	sbcth	⊢ ( 𝑥 ∈ V → [ 𝑥 / 𝑎 ] ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 ↔ 𝜒 ) ) )
3		sbcim1	⊢ ( [ 𝑥 / 𝑎 ] ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 ↔ 𝜒 ) ) → ( [ 𝑥 / 𝑎 ] 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → [ 𝑥 / 𝑎 ] ( 𝜑 ↔ 𝜒 ) ) )
4	2 3	syl	⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑎 ] 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → [ 𝑥 / 𝑎 ] ( 𝜑 ↔ 𝜒 ) ) )
5		sbceq2g	⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑎 ] 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑝 = ⦋ 𝑥 / 𝑎 ⦌ ⟨ 𝑎 , 𝑏 ⟩ ) )
6		csbopg	⊢ ( 𝑥 ∈ V → ⦋ 𝑥 / 𝑎 ⦌ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ⦋ 𝑥 / 𝑎 ⦌ 𝑎 , ⦋ 𝑥 / 𝑎 ⦌ 𝑏 ⟩ )
7		csbvarg	⊢ ( 𝑥 ∈ V → ⦋ 𝑥 / 𝑎 ⦌ 𝑎 = 𝑥 )
8		csbconstg	⊢ ( 𝑥 ∈ V → ⦋ 𝑥 / 𝑎 ⦌ 𝑏 = 𝑏 )
9	7 8	opeq12d	⊢ ( 𝑥 ∈ V → ⟨ ⦋ 𝑥 / 𝑎 ⦌ 𝑎 , ⦋ 𝑥 / 𝑎 ⦌ 𝑏 ⟩ = ⟨ 𝑥 , 𝑏 ⟩ )
10	6 9	eqtrd	⊢ ( 𝑥 ∈ V → ⦋ 𝑥 / 𝑎 ⦌ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑏 ⟩ )
11	10	eqeq2d	⊢ ( 𝑥 ∈ V → ( 𝑝 = ⦋ 𝑥 / 𝑎 ⦌ ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ ) )
12	5 11	bitrd	⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑎 ] 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ ) )
13		sbcbig	⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑎 ] ( 𝜑 ↔ 𝜒 ) ↔ ( [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) )
14		sbcg	⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) )
15	14	bibi1d	⊢ ( 𝑥 ∈ V → ( ( [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ↔ ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) )
16	13 15	bitrd	⊢ ( 𝑥 ∈ V → ( [ 𝑥 / 𝑎 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) )
17	4 12 16	3imtr3d	⊢ ( 𝑥 ∈ V → ( 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ → ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) )
18	17	elv	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ → ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) )
19	18	sbcth	⊢ ( 𝑦 ∈ V → [ 𝑦 / 𝑏 ] ( 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ → ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) )
20		sbcim1	⊢ ( [ 𝑦 / 𝑏 ] ( 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ → ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) → ( [ 𝑦 / 𝑏 ] 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ → [ 𝑦 / 𝑏 ] ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) )
21	19 20	syl	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑏 ] 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ → [ 𝑦 / 𝑏 ] ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ) )
22		sbceq2g	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑏 ] 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ ↔ 𝑝 = ⦋ 𝑦 / 𝑏 ⦌ ⟨ 𝑥 , 𝑏 ⟩ ) )
23		csbopg	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑏 ⦌ ⟨ 𝑥 , 𝑏 ⟩ = ⟨ ⦋ 𝑦 / 𝑏 ⦌ 𝑥 , ⦋ 𝑦 / 𝑏 ⦌ 𝑏 ⟩ )
24		csbconstg	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑏 ⦌ 𝑥 = 𝑥 )
25		csbvarg	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑏 ⦌ 𝑏 = 𝑦 )
26	24 25	opeq12d	⊢ ( 𝑦 ∈ V → ⟨ ⦋ 𝑦 / 𝑏 ⦌ 𝑥 , ⦋ 𝑦 / 𝑏 ⦌ 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
27	23 26	eqtrd	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑏 ⦌ ⟨ 𝑥 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
28	27	eqeq2d	⊢ ( 𝑦 ∈ V → ( 𝑝 = ⦋ 𝑦 / 𝑏 ⦌ ⟨ 𝑥 , 𝑏 ⟩ ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
29	22 28	bitrd	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑏 ] 𝑝 = ⟨ 𝑥 , 𝑏 ⟩ ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
30		sbcbig	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑏 ] ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ↔ ( [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜒 ) ) )
31		sbcg	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
32	31	bibi1d	⊢ ( 𝑦 ∈ V → ( ( [ 𝑦 / 𝑏 ] 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜒 ) ↔ ( 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜒 ) ) )
33	30 32	bitrd	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑏 ] ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜒 ) ↔ ( 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜒 ) ) )
34	21 29 33	3imtr3d	⊢ ( 𝑦 ∈ V → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜒 ) ) )
35	34	elv	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜒 ) )