Theorem eliin 4946

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∩ ciin 4942

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-iin 4944

This theorem is referenced by:  iinconst  4952  iuniin  4954  iinssiun  4955  iinss1  4957  ssiinf  5003  iinss  5005  iinss2  5006  iinab  5016  iinun2  5021  iundif2  5022  iindif1  5023  iindif2  5025  iinin2  5026  elriin  5029  iinpw  5054  triin  5214  xpiindi  5775  cnviin  6233  iinpreima  7002  iiner  8713  ixpiin  8848  boxriin  8864  iunocv  21616  hauscmplem  23319  txtube  23553  isfcls  23922  iscmet3  25218  taylfval  26291  zarclsiin  33879  fnemeet1  36399  diaglbN  41093  dibglbN  41204  dihglbcpreN  41338  kelac1  43095  eliind  45107  eliuniin  45135  eliin2f  45140  eliinid  45147  eliuniin2  45156  iinssiin  45165  eliind2  45166  iinssf  45174  iindif2f  45196  allbutfi  45430  meaiininclem  46523  hspdifhsp  46653  iinhoiicclem  46710  preimageiingt  46757  preimaleiinlt  46758  smflimlem2  46809  smflimsuplem5  46861  smflimsuplem7  46863  iineq0  48850  iinxp  48861  iinfsubc  49089