Metamath Proof Explorer

Theorem dfin4

Description: Alternate definition of the intersection of two classes. Exercise 4.10(q) of Mendelson p. 231. (Contributed by NM, 25-Nov-2003)

Ref Expression
Assertion dfin4 A B = A A B


Step Hyp Ref Expression
1 inss1 A B A
2 dfss4 A B A A A A B = A B
3 1 2 mpbi A A A B = A B
4 difin A A B = A B
5 4 difeq2i A A A B = A A B
6 3 5 eqtr3i A B = A A B