Theorem eliin 4956

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 2849	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
2	1	ralbidv 3186	. 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
3		df-iin 4954	. 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
4	2, 3	elab2g 3634	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∩ ciin 4952

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-iin 4954

This theorem is used by:  iinconst  4962  iuniin  4964  iinssiun  4965  iinss1  4967  ssiinf  5013  iinss  5015  iinss2  5016  iinab  5026  iinun2  5031  iundif2  5032  iindif1  5035  iindif2  5037  iinin2  5038  elriin  5041  iinpw  5066  triin  5229  xpiindi  5812  cnviin  6282  iinpreima  7061  iiner  8794  ixpiin  8936  boxriin  8952  iunocv  21967  hauscmplem  23704  txtube  23939  isfcls  24308  iscmet3  25594  taylfval  26668  suppgsumssiun  33615  zarclsiin  34485  fnemeet1  37124  diaglbN  42080  dibglbN  42191  dihglbcpreN  42325  kelac1  44023  eliind  46031  eliuniin  46057  eliin2f  46062  eliinid  46069  eliuniin2  46078  iinssiin  46087  eliind2  46088  iinssf  46096  iindif2f  46118  allbutfi  46348  meaiininclem  47440  hspdifhsp  47570  iinhoiicclem  47627  preimageiingt  47674  preimaleiinlt  47675  smflimlem2  47726  smflimsuplem5  47778  smflimsuplem7  47780  iineq0  49874  iinxp  49885  iinfsubc  50110