Theorem eliin 4966

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∀wral 3082  ∩ ciin 4962

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-iin 4964

This theorem is used by:  iinconst  4972  iuniin  4974  iinssiun  4975  iinss1  4977  ssiinf  5024  iinss  5026  iinss2  5027  iinab  5037  iinun2  5042  iundif2  5043  iindif1  5046  iindif2  5048  iinin2  5049  elriin  5052  iinpw  5077  triin  5240  xpiindi  5826  cnviin  6294  iinpreima  7071  iiner  8796  ixpiin  8931  boxriin  8947  iunocv  21868  hauscmplem  23600  txtube  23834  isfcls  24203  iscmet3  25489  taylfval  26559  suppgsumssiun  33423  zarclsiin  34292  fnemeet1  36918  diaglbN  41870  dibglbN  41981  dihglbcpreN  42115  kelac1  43831  eliind  45832  eliuniin  45858  eliin2f  45863  eliinid  45870  eliuniin2  45879  iinssiin  45888  eliind2  45889  iinssf  45897  iindif2f  45919  allbutfi  46149  meaiininclem  47241  hspdifhsp  47371  iinhoiicclem  47428  preimageiingt  47475  preimaleiinlt  47476  smflimlem2  47527  smflimsuplem5  47579  smflimsuplem7  47581  iineq0  49639  iinxp  49650  iinfsubc  49877