Theorem eliin 5003

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∩ ciin 4999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-iin 5001

This theorem is referenced by:  iinconst  5008  iuniin  5010  iinssiun  5011  iinss1  5013  ssiinf  5058  iinss  5060  iinss2  5061  iinab  5072  iinun2  5077  iundif2  5078  iindif1  5079  iindif2  5081  iinin2  5082  elriin  5085  iinpw  5110  triin  5283  xpiindi  5836  cnviin  6286  iinpreima  7071  iiner  8783  ixpiin  8918  boxriin  8934  iunocv  21234  hauscmplem  22910  txtube  23144  isfcls  23513  iscmet3  24810  taylfval  25871  zarclsiin  32851  fnemeet1  35251  diaglbN  39926  dibglbN  40037  dihglbcpreN  40171  kelac1  41805  eliind  43758  eliuniin  43788  eliin2f  43793  eliinid  43800  eliuniin2  43809  iinssiin  43818  eliind2  43819  iinssf  43827  iindif2f  43854  allbutfi  44103  meaiininclem  45202  hspdifhsp  45332  iinhoiicclem  45389  preimageiingt  45436  preimaleiinlt  45437  smflimlem2  45488  smflimsuplem5  45540  smflimsuplem7  45542