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 A C = B C


Step Hyp Ref Expression
1 eleq2 A = B x A x B
2 1 anbi1d A = B x A x C x B x C
3 elin x A C x A x C
4 elin x B C x B x C
5 2 3 4 3bitr4g A = B x A C x B C
6 5 eqrdv A = B A C = B C