Theorem eliin 4951

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∩ ciin 4947

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-iin 4949

This theorem is referenced by:  iinconst  4957  iuniin  4959  iinssiun  4960  iinss1  4962  ssiinf  5010  iinss  5012  iinss2  5013  iinab  5023  iinun2  5028  iundif2  5029  iindif1  5030  iindif2  5032  iinin2  5033  elriin  5036  iinpw  5061  triin  5221  xpiindi  5784  cnviin  6244  iinpreima  7014  iiner  8726  ixpiin  8862  boxriin  8878  iunocv  21636  hauscmplem  23350  txtube  23584  isfcls  23953  iscmet3  25249  taylfval  26322  zarclsiin  34028  fnemeet1  36560  diaglbN  41311  dibglbN  41422  dihglbcpreN  41556  kelac1  43301  eliind  45312  eliuniin  45339  eliin2f  45344  eliinid  45351  eliuniin2  45360  iinssiin  45369  eliind2  45370  iinssf  45378  iindif2f  45400  allbutfi  45633  meaiininclem  46726  hspdifhsp  46856  iinhoiicclem  46913  preimageiingt  46960  preimaleiinlt  46961  smflimlem2  47012  smflimsuplem5  47064  smflimsuplem7  47066  iineq0  49061  iinxp  49072  iinfsubc  49299