Theorem eliin 4927

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∩ ciin 4923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-iin 4925

This theorem is referenced by:  iinconst  4933  iuniin  4935  iinssiun  4936  iinss1  4938  ssiinf  4985  iinss  4987  iinss2  4988  iinab  4998  iinun2  5003  iundif2  5004  iindif1  5005  iindif2  5007  iinin2  5008  elriin  5011  iinpw  5036  triin  5197  xpiindi  5778  cnviin  6238  iinpreima  7011  iiner  8727  ixpiin  8863  boxriin  8879  iunocv  21657  hauscmplem  23390  txtube  23624  isfcls  23993  iscmet3  25279  taylfval  26343  suppgsumssiun  33154  zarclsiin  34064  fnemeet1  36603  diaglbN  41556  dibglbN  41667  dihglbcpreN  41801  kelac1  43517  eliind  45528  eliuniin  45554  eliin2f  45559  eliinid  45566  eliuniin2  45575  iinssiin  45584  eliind2  45585  iinssf  45593  iindif2f  45615  allbutfi  45845  meaiininclem  46937  hspdifhsp  47067  iinhoiicclem  47124  preimageiingt  47171  preimaleiinlt  47172  smflimlem2  47223  smflimsuplem5  47275  smflimsuplem7  47277  iineq0  49318  iinxp  49329  iinfsubc  49556