Theorem eliin 4963

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∩ ciin 4959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-iin 4961

This theorem is referenced by:  iinconst  4969  iuniin  4971  iinssiun  4972  iinss1  4974  ssiinf  5021  iinss  5023  iinss2  5024  iinab  5035  iinun2  5040  iundif2  5041  iindif1  5042  iindif2  5044  iinin2  5045  elriin  5048  iinpw  5073  triin  5234  xpiindi  5802  cnviin  6262  iinpreima  7044  iiner  8765  ixpiin  8900  boxriin  8916  iunocv  21597  hauscmplem  23300  txtube  23534  isfcls  23903  iscmet3  25200  taylfval  26273  zarclsiin  33868  fnemeet1  36361  diaglbN  41056  dibglbN  41167  dihglbcpreN  41301  kelac1  43059  eliind  45072  eliuniin  45100  eliin2f  45105  eliinid  45112  eliuniin2  45121  iinssiin  45130  eliind2  45131  iinssf  45139  iindif2f  45161  allbutfi  45396  meaiininclem  46491  hspdifhsp  46621  iinhoiicclem  46678  preimageiingt  46725  preimaleiinlt  46726  smflimlem2  46777  smflimsuplem5  46829  smflimsuplem7  46831  iineq0  48812  iinxp  48823  iinfsubc  49051