Metamath Proof Explorer

Theorem ineq1OLD

Description: Obsolete version of ineq1 as of 20-Sep-2023. Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ineq1OLD	$⊢ A = B \to A \cap C = B \cap C$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ A = B \to (x \in A \leftrightarrow x \in B)$
2	1	anbi1d	$⊢ A = B \to ((x \in A \land x \in C) \leftrightarrow (x \in B \land x \in C))$
3		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
4		elin	$⊢ x \in (B \cap C) \leftrightarrow (x \in B \land x \in C)$
5	2 3 4	3bitr4g	$⊢ A = B \to (x \in (A \cap C) \leftrightarrow x \in (B \cap C))$
6	5	eqrdv	$⊢ A = B \to A \cap C = B \cap C$