Theorem eliin 4996

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∩ ciin 4992

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-iin 4994

This theorem is referenced by:  iinconst  5002  iuniin  5004  iinssiun  5005  iinss1  5007  ssiinf  5054  iinss  5056  iinss2  5057  iinab  5068  iinun2  5073  iundif2  5074  iindif1  5075  iindif2  5077  iinin2  5078  elriin  5081  iinpw  5106  triin  5276  xpiindi  5846  cnviin  6306  iinpreima  7089  iiner  8829  ixpiin  8964  boxriin  8980  iunocv  21699  hauscmplem  23414  txtube  23648  isfcls  24017  iscmet3  25327  taylfval  26400  zarclsiin  33870  fnemeet1  36367  diaglbN  41057  dibglbN  41168  dihglbcpreN  41302  kelac1  43075  eliind  45076  eliuniin  45104  eliin2f  45109  eliinid  45116  eliuniin2  45125  iinssiin  45134  eliind2  45135  iinssf  45143  iindif2f  45165  allbutfi  45404  meaiininclem  46501  hspdifhsp  46631  iinhoiicclem  46688  preimageiingt  46735  preimaleiinlt  46736  smflimlem2  46787  smflimsuplem5  46839  smflimsuplem7  46841