Theorem eliin 4962

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∩ ciin 4958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-iin 4960

This theorem is referenced by:  iinconst  4968  iuniin  4970  iinssiun  4971  iinss1  4973  ssiinf  5020  iinss  5022  iinss2  5023  iinab  5033  iinun2  5038  iundif2  5039  iindif1  5042  iindif2  5044  iinin2  5045  elriin  5048  iinpw  5073  triin  5236  xpiindi  5823  cnviin  6289  iinpreima  7066  iiner  8788  ixpiin  8923  boxriin  8939  iunocv  21812  hauscmplem  23544  txtube  23778  isfcls  24147  iscmet3  25433  taylfval  26500  suppgsumssiun  33370  zarclsiin  34239  fnemeet1  36855  diaglbN  41807  dibglbN  41918  dihglbcpreN  42052  kelac1  43770  eliind  45771  eliuniin  45797  eliin2f  45802  eliinid  45809  eliuniin2  45818  iinssiin  45827  eliind2  45828  iinssf  45836  iindif2f  45858  allbutfi  46088  meaiininclem  47180  hspdifhsp  47310  iinhoiicclem  47367  preimageiingt  47414  preimaleiinlt  47415  smflimlem2  47466  smflimsuplem5  47518  smflimsuplem7  47520  iineq0  49575  iinxp  49586  iinfsubc  49813