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

Metamath Proof Explorer

Theorem sbcopeq1a

Description: Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a that avoids the existential quantifiers of copsexg ). (Contributed by NM, 19-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion sbcopeq1a ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( [ ( 1st ‘ 𝐴 ) / 𝑥 ] [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ↔ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 vex ⊢ 𝑦 ∈ V
3 1 2 op2ndd ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑦 )
4 3 eqcomd ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑦 = ( 2nd ‘ 𝐴 ) )
5 sbceq1a ⊢ ( 𝑦 = ( 2nd ‘ 𝐴 ) → ( 𝜑 ↔ [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ) )
6 4 5 syl ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ) )
7 1 2 op1std ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝐴 ) = 𝑥 )
8 7 eqcomd ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑥 = ( 1st ‘ 𝐴 ) )
9 sbceq1a ⊢ ( 𝑥 = ( 1st ‘ 𝐴 ) → ( [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ↔ [ ( 1st ‘ 𝐴 ) / 𝑥 ] [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ) )
10 8 9 syl ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ↔ [ ( 1st ‘ 𝐴 ) / 𝑥 ] [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ) )
11 6 10 bitr2d ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( [ ( 1st ‘ 𝐴 ) / 𝑥 ] [ ( 2nd ‘ 𝐴 ) / 𝑦 ] 𝜑 ↔ 𝜑 ) )