Metamath Proof Explorer

Theorem dfin5

Description: Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005)

Ref Expression
Assertion dfin5 A B = x A | x B


Step Hyp Ref Expression
1 df-in A B = x | x A x B
2 df-rab x A | x B = x | x A x B
3 1 2 eqtr4i A B = x A | x B