Theorem eliin 5002

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  ∀wral 3060  ∩ ciin 4998

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-iin 5000

This theorem is referenced by:  iinconst  5007  iuniin  5009  iinssiun  5010  iinss1  5012  ssiinf  5057  iinss  5059  iinss2  5060  iinab  5071  iinun2  5076  iundif2  5077  iindif1  5078  iindif2  5080  iinin2  5081  elriin  5084  iinpw  5109  triin  5282  xpiindi  5835  cnviin  6285  iinpreima  7070  iiner  8789  ixpiin  8924  boxriin  8940  iunocv  21545  hauscmplem  23231  txtube  23465  isfcls  23834  iscmet3  25142  taylfval  26211  zarclsiin  33317  fnemeet1  35718  diaglbN  40393  dibglbN  40504  dihglbcpreN  40638  kelac1  42271  eliind  44223  eliuniin  44253  eliin2f  44258  eliinid  44265  eliuniin2  44274  iinssiin  44283  eliind2  44284  iinssf  44292  iindif2f  44319  allbutfi  44565  meaiininclem  45664  hspdifhsp  45794  iinhoiicclem  45851  preimageiingt  45898  preimaleiinlt  45899  smflimlem2  45950  smflimsuplem5  46002  smflimsuplem7  46004