Metamath Proof Explorer

Theorem intiin

Description: Class intersection in terms of indexed intersection. Definition in Stoll p. 44. (Contributed by NM, 28-Jun-1998)

Ref Expression
Assertion intiin 
|- |^| A = |^|_ x e. A x

Proof

Step Hyp Ref Expression
1 dfint2 
 |-  |^| A = { y | A. x e. A y e. x }
2 df-iin 
 |-  |^|_ x e. A x = { y | A. x e. A y e. x }
3 1 2 eqtr4i 
 |-  |^| A = |^|_ x e. A x