Theorem eliin 4953

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ∩ ciin 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-iin 4951

This theorem is referenced by:  iinconst  4959  iuniin  4961  iinssiun  4962  iinss1  4964  ssiinf  5011  iinss  5013  iinss2  5014  iinab  5024  iinun2  5029  iundif2  5030  iindif1  5031  iindif2  5033  iinin2  5034  elriin  5037  iinpw  5062  triin  5223  xpiindi  5805  cnviin  6269  iinpreima  7046  iiner  8766  ixpiin  8902  boxriin  8918  iunocv  21713  hauscmplem  23446  txtube  23680  isfcls  24049  iscmet3  25335  taylfval  26399  suppgsumssiun  33213  zarclsiin  34129  fnemeet1  36690  diaglbN  41643  dibglbN  41754  dihglbcpreN  41888  kelac1  43604  eliind  45615  eliuniin  45641  eliin2f  45646  eliinid  45653  eliuniin2  45662  iinssiin  45671  eliind2  45672  iinssf  45680  iindif2f  45702  allbutfi  45932  meaiininclem  47024  hspdifhsp  47154  iinhoiicclem  47211  preimageiingt  47258  preimaleiinlt  47259  smflimlem2  47310  smflimsuplem5  47362  smflimsuplem7  47364  iineq0  49405  iinxp  49416  iinfsubc  49643