Theorem intiin 5023

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

Assertion

Ref	Expression
intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥

Distinct variable group:   𝑥,𝐴

Proof of Theorem intiin

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfint2 4914	. 2 ⊢ ∩ 𝐴 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
2		df-iin 4959	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝑥 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
3	1, 2	eqtr4i 2789	1 ⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥

This proof depends on syntax axioms:   = wceq 1570  {cab 2741  ∀wral 3080  ∩ cint 4912  ∩ ciin 4957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-int 4913  df-iin 4959

This theorem is used by:  trint  5236  relint  5806  intpreima  7102  ixpint  8991  firest  17653  efger  19983  subdrgint  21111  rintopn  23282  intcld  23413  iundifdifd  33254  iundifdif  33255  intxpd  50274