This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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