Metamath Proof Explorer


Theorem dfiin2

Description: Alternate definition of indexed intersection when B is a set. Definition 15(b) of Suppes p. 44. (Contributed by NM, 28-Jun-1998) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Hypothesis dfiun2.1 BV
Assertion dfiin2 xAB=y|xAy=B

Proof

Step Hyp Ref Expression
1 dfiun2.1 BV
2 dfiin2g xABVxAB=y|xAy=B
3 1 a1i xABV
4 2 3 mprg xAB=y|xAy=B