Metamath Proof Explorer

Theorem mpteq2iaOLD

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

Ref Expression
Hypothesis mpteq2ia.1 ⊢ x ∈ A → B = C
Assertion mpteq2iaOLD ⊢ x ∈ A ⟼ B = x ∈ A ⟼ C

Proof

Step Hyp Ref Expression
1 mpteq2ia.1 ⊢ x ∈ A → B = C
2 eqid ⊢ A = A
3 2 ax-gen ⊢ ∀ x A = A
4 1 rgen ⊢ ∀ x ∈ A B = C
5 mpteq12f ⊢ ∀ x A = A ∧ ∀ x ∈ A B = C → x ∈ A ⟼ B = x ∈ A ⟼ C
6 3 4 5 mp2an ⊢ x ∈ A ⟼ B = x ∈ A ⟼ C