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

Proof

Step	Hyp	Ref	Expression
1		sbcop.z	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2	1	sbcop1	⊢ ( [ 𝑎 / 𝑥 ] 𝜓 ↔ [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 )
3	2	sbcbii	⊢ ( [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ↔ [ 𝑏 / 𝑦 ] [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 )
4		sbcnestgw	⊢ ( 𝑏 ∈ V → ( [ 𝑏 / 𝑦 ] [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 ↔ [ ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 ) )
5	4	elv	⊢ ( [ 𝑏 / 𝑦 ] [ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 ↔ [ ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 )
6		csbopg	⊢ ( 𝑏 ∈ V → ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ = ⟨ ⦋ 𝑏 / 𝑦 ⦌ 𝑎 , ⦋ 𝑏 / 𝑦 ⦌ 𝑦 ⟩ )
7	6	elv	⊢ ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ = ⟨ ⦋ 𝑏 / 𝑦 ⦌ 𝑎 , ⦋ 𝑏 / 𝑦 ⦌ 𝑦 ⟩
8		vex	⊢ 𝑏 ∈ V
9	8	csbconstgi	⊢ ⦋ 𝑏 / 𝑦 ⦌ 𝑎 = 𝑎
10	8	csbvargi	⊢ ⦋ 𝑏 / 𝑦 ⦌ 𝑦 = 𝑏
11	9 10	opeq12i	⊢ ⟨ ⦋ 𝑏 / 𝑦 ⦌ 𝑎 , ⦋ 𝑏 / 𝑦 ⦌ 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩
12	7 11	eqtri	⊢ ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩
13		dfsbcq	⊢ ( ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → ( [ ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 ↔ [ ⟨ 𝑎 , 𝑏 ⟩ / 𝑧 ] 𝜑 ) )
14	12 13	ax-mp	⊢ ( [ ⦋ 𝑏 / 𝑦 ⦌ ⟨ 𝑎 , 𝑦 ⟩ / 𝑧 ] 𝜑 ↔ [ ⟨ 𝑎 , 𝑏 ⟩ / 𝑧 ] 𝜑 )
15	3 5 14	3bitri	⊢ ( [ 𝑏 / 𝑦 ] [ 𝑎 / 𝑥 ] 𝜓 ↔ [ ⟨ 𝑎 , 𝑏 ⟩ / 𝑧 ] 𝜑 )