Theorem intiin 4324

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

Assertion

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

Distinct variable group:   x, A

Proof of Theorem intiin

Dummy variable y is distinct from all other variables.

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

Syntax hints:   = wceq 1405   {cab 2387   A.wral 2753   |^|cint 4226   |^|_ciin 4271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-ral 2758  df-int 4227  df-iin 4273

This theorem is referenced by:  relint  4945  intpreima  5995  ixpint  7533  firest  15045  efger  17058  rintopn  19708  intcld  19831  iundifdifd  27845  iundifdif  27846