Theorem eliin 4960

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

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

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 4958

This theorem is referenced by:  iinconst  4966  iuniin  4968  iinssiun  4969  iinss1  4971  ssiinf  5018  iinss  5020  iinss2  5021  iinab  5032  iinun2  5037  iundif2  5038  iindif1  5039  iindif2  5041  iinin2  5042  elriin  5045  iinpw  5070  triin  5231  xpiindi  5799  cnviin  6259  iinpreima  7041  iiner  8762  ixpiin  8897  boxriin  8913  iunocv  21590  hauscmplem  23293  txtube  23527  isfcls  23896  iscmet3  25193  taylfval  26266  zarclsiin  33861  fnemeet1  36354  diaglbN  41049  dibglbN  41160  dihglbcpreN  41294  kelac1  43052  eliind  45065  eliuniin  45093  eliin2f  45098  eliinid  45105  eliuniin2  45114  iinssiin  45123  eliind2  45124  iinssf  45132  iindif2f  45154  allbutfi  45389  meaiininclem  46484  hspdifhsp  46614  iinhoiicclem  46671  preimageiingt  46718  preimaleiinlt  46719  smflimlem2  46770  smflimsuplem5  46822  smflimsuplem7  46824  iineq0  48808  iinxp  48819  iinfsubc  49047