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

Metamath Proof Explorer

Theorem cic1st2ndbr

Description: Rewrite the predicate of isomorphic objects with separated parts. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion cic1st2ndbr ⊢ P ∈ ≃ 𝑐 ⁡ C → 1 st ⁡ P ≃ 𝑐 ⁡ C 2 nd ⁡ P

Proof

Step Hyp Ref Expression
1 cic1st2nd ⊢ P ∈ ≃ 𝑐 ⁡ C → P = 1 st ⁡ P 2 nd ⁡ P
2 id ⊢ P ∈ ≃ 𝑐 ⁡ C → P ∈ ≃ 𝑐 ⁡ C
3 1 2 eqeltrrd ⊢ P ∈ ≃ 𝑐 ⁡ C → 1 st ⁡ P 2 nd ⁡ P ∈ ≃ 𝑐 ⁡ C
4 df-br ⊢ 1 st ⁡ P ≃ 𝑐 ⁡ C 2 nd ⁡ P ↔ 1 st ⁡ P 2 nd ⁡ P ∈ ≃ 𝑐 ⁡ C
5 3 4 sylibr ⊢ P ∈ ≃ 𝑐 ⁡ C → 1 st ⁡ P ≃ 𝑐 ⁡ C 2 nd ⁡ P