Theorem eliin 4933

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

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

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 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-iin 4931

This theorem is referenced by:  iinconst  4939  iuniin  4941  iinssiun  4942  iinss1  4944  ssiinf  4991  iinss  4993  iinss2  4994  iinab  5004  iinun2  5009  iundif2  5010  iindif1  5011  iindif2  5013  iinin2  5014  elriin  5017  iinpw  5042  triin  5203  xpiindi  5784  cnviin  6244  iinpreima  7017  iiner  8733  ixpiin  8869  boxriin  8885  iunocv  21663  hauscmplem  23396  txtube  23630  isfcls  23999  iscmet3  25285  taylfval  26349  suppgsumssiun  33160  zarclsiin  34062  fnemeet1  36601  diaglbN  41554  dibglbN  41665  dihglbcpreN  41799  kelac1  43515  eliind  45526  eliuniin  45553  eliin2f  45558  eliinid  45565  eliuniin2  45574  iinssiin  45583  eliind2  45584  iinssf  45592  iindif2f  45614  allbutfi  45844  meaiininclem  46936  hspdifhsp  47066  iinhoiicclem  47123  preimageiingt  47170  preimaleiinlt  47171  smflimlem2  47222  smflimsuplem5  47274  smflimsuplem7  47276  iineq0  49317  iinxp  49328  iinfsubc  49555