Theorem eliin 4959

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∩ ciin 4955

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-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-iin 4957

This theorem is used by:  iinconst  4965  iuniin  4967  iinssiun  4968  iinss1  4970  ssiinf  5016  iinss  5018  iinss2  5019  iinab  5029  iinun2  5034  iundif2  5035  iindif1  5038  iindif2  5040  iinin2  5041  elriin  5044  iinpw  5069  triin  5233  xpiindi  5819  cnviin  6308  iinpreima  7096  iiner  8841  ixpiin  8983  boxriin  8999  iunocv  22020  hauscmplem  23757  txtube  23992  isfcls  24361  iscmet3  25647  taylfval  26719  suppgsumssiun  33709  zarclsiin  34586  fnemeet1  37345  diaglbN  42315  dibglbN  42426  dihglbcpreN  42560  kelac1  44269  eliind  46304  eliuniin  46329  eliin2f  46334  eliinid  46341  eliuniin2  46350  iinssiin  46359  eliind2  46360  iinssf  46368  iindif2f  46390  allbutfi  46619  meaiininclem  47711  hspdifhsp  47841  iinhoiicclem  47898  preimageiingt  47945  preimaleiinlt  47946  smflimlem2  47997  smflimsuplem5  48049  smflimsuplem7  48051  iineq0  50146  iinxp  50157  iinfsubc  50387