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=xAx

Proof

Step Hyp Ref Expression
1 dfint2 A=y|xAyx
2 df-iin xAx=y|xAyx
3 1 2 eqtr4i A=xAx