Metamath Proof Explorer

Theorem mpteq2daOLD

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

Ref Expression
Hypotheses mpteq2da.1 ⊢ Ⅎ x φ
mpteq2da.2 ⊢ φ ∧ x ∈ A → B = C
Assertion mpteq2daOLD ⊢ φ → x ∈ A ⟼ B = x ∈ A ⟼ C

Proof

Step Hyp Ref Expression
1 mpteq2da.1 ⊢ Ⅎ x φ
2 mpteq2da.2 ⊢ φ ∧ x ∈ A → B = C
3 eqid ⊢ A = A
4 3 ax-gen ⊢ ∀ x A = A
5 2 ex ⊢ φ → x ∈ A → B = C
6 1 5 ralrimi ⊢ φ → ∀ x ∈ A B = C
7 mpteq12f ⊢ ∀ x A = A ∧ ∀ x ∈ A B = C → x ∈ A ⟼ B = x ∈ A ⟼ C
8 4 6 7 sylancr ⊢ φ → x ∈ A ⟼ B = x ∈ A ⟼ C