Metamath Proof Explorer

Theorem mpteq1OLD

Description: Obsolete version of mpteq1 as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion mpteq1OLD ⊢ A = B → x ∈ A ⟼ C = x ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 eqidd ⊢ x ∈ A → C = C
2 1 rgen ⊢ ∀ x ∈ A C = C
3 mpteq12 ⊢ A = B ∧ ∀ x ∈ A C = C → x ∈ A ⟼ C = x ∈ B ⟼ C
4 2 3 mpan2 ⊢ A = B → x ∈ A ⟼ C = x ∈ B ⟼ C