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 \in A \to B = C$
	Assertion	mpteq2iaOLD	$⊢ (x \in A ⟼ B) = (x \in A ⟼ C)$

Proof

Step	Hyp	Ref	Expression
1		mpteq2ia.1	$⊢ x \in A \to B = C$
2		eqid	$⊢ A = A$
3	2	ax-gen	$⊢ \forall x A = A$
4	1	rgen	$⊢ \forall x \in A B = C$
5		mpteq12f	$⊢ (\forall x A = A \land \forall x \in A B = C) \to (x \in A ⟼ B) = (x \in A ⟼ C)$
6	3 4 5	mp2an	$⊢ (x \in A ⟼ B) = (x \in A ⟼ C)$