Theorem eliin 4949

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-iin 4947

This theorem is referenced by:  iinconst  4955  iuniin  4957  iinssiun  4958  iinss1  4960  ssiinf  5006  iinss  5008  iinss2  5009  iinab  5020  iinun2  5025  iundif2  5026  iindif1  5027  iindif2  5029  iinin2  5030  elriin  5033  iinpw  5058  triin  5218  xpiindi  5782  cnviin  6238  iinpreima  7007  iiner  8723  ixpiin  8858  boxriin  8874  iunocv  21606  hauscmplem  23309  txtube  23543  isfcls  23912  iscmet3  25209  taylfval  26282  zarclsiin  33837  fnemeet1  36339  diaglbN  41034  dibglbN  41145  dihglbcpreN  41279  kelac1  43036  eliind  45049  eliuniin  45077  eliin2f  45082  eliinid  45089  eliuniin2  45098  iinssiin  45107  eliind2  45108  iinssf  45116  iindif2f  45138  allbutfi  45373  meaiininclem  46468  hspdifhsp  46598  iinhoiicclem  46655  preimageiingt  46702  preimaleiinlt  46703  smflimlem2  46754  smflimsuplem5  46806  smflimsuplem7  46808  iineq0  48805  iinxp  48816  iinfsubc  49044