Theorem eliin 4461

Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
eliin	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem eliin

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2676	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
2	1	ralbidv 2969	. 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
3		df-iin 4458	. 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
4	2, 3	elab2g 3322	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∩ ciin 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-iin 4458

This theorem is referenced by:  iinconst  4466  iuniin  4467  iinss1  4469  ssiinf  4505  iinss  4507  iinss2  4508  iinab  4517  iinun2  4522  iundif2  4523  iindif2  4525  iinin2  4526  elriin  4529  iinpw  4550  xpiindi  5179  cnviin  5589  iinpreima  6253  iiner  7706  ixpiin  7820  boxriin  7836  iunocv  19844  hauscmplem  21019  txtube  21253  isfcls  21623  iscmet3  22899  taylfval  23917  fnemeet1  31531  diaglbN  35362  dibglbN  35473  dihglbcpreN  35607  kelac1  36651  eliind  38266  eliuniin  38307  eliin2f  38316  eliinid  38325  eliuniin2  38335  allbutfi  38557  meaiininclem  39376  hspdifhsp  39506  iinhoiicclem  39564  preimageiingt  39607  preimaleiinlt  39608  smflimlem2  39658