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 i^i B ) = { x e. A | x e. B }

Proof

Step Hyp Ref Expression
1 df-in 
 |-  ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
2 df-rab 
 |-  { x e. A | x e. B } = { x | ( x e. A /\ x e. B ) }
3 1 2 eqtr4i 
 |-  ( A i^i B ) = { x e. A | x e. B }