Theorem eliin 4946

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ∩ ciin 4942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-iin 4944

This theorem is referenced by:  iinconst  4952  iuniin  4954  iinssiun  4955  iinss1  4957  ssiinf  5005  iinss  5007  iinss2  5008  iinab  5018  iinun2  5023  iundif2  5024  iindif1  5025  iindif2  5027  iinin2  5028  elriin  5031  iinpw  5056  triin  5216  xpiindi  5779  cnviin  6238  iinpreima  7008  iiner  8719  ixpiin  8854  boxriin  8870  iunocv  21620  hauscmplem  23322  txtube  23556  isfcls  23925  iscmet3  25221  taylfval  26294  zarclsiin  33905  fnemeet1  36431  diaglbN  41174  dibglbN  41285  dihglbcpreN  41419  kelac1  43180  eliind  45192  eliuniin  45220  eliin2f  45225  eliinid  45232  eliuniin2  45241  iinssiin  45250  eliind2  45251  iinssf  45259  iindif2f  45281  allbutfi  45515  meaiininclem  46608  hspdifhsp  46738  iinhoiicclem  46795  preimageiingt  46842  preimaleiinlt  46843  smflimlem2  46894  smflimsuplem5  46946  smflimsuplem7  46948  iineq0  48944  iinxp  48955  iinfsubc  49183