Theorem eliin 4929

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∩ ciin 4925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-iin 4927

This theorem is referenced by:  iinconst  4934  iuniin  4936  iinssiun  4937  iinss1  4939  ssiinf  4984  iinss  4986  iinss2  4987  iinab  4997  iinun2  5002  iundif2  5003  iindif1  5004  iindif2  5006  iinin2  5007  elriin  5010  iinpw  5035  triin  5206  xpiindi  5744  cnviin  6189  iinpreima  6946  iiner  8578  ixpiin  8712  boxriin  8728  iunocv  20886  hauscmplem  22557  txtube  22791  isfcls  23160  iscmet3  24457  taylfval  25518  zarclsiin  31821  fnemeet1  34555  diaglbN  39069  dibglbN  39180  dihglbcpreN  39314  kelac1  40888  eliind  42619  eliuniin  42649  eliin2f  42654  eliinid  42661  eliuniin2  42669  iinssiin  42678  eliind2  42679  iinssf  42687  allbutfi  42933  meaiininclem  44024  hspdifhsp  44154  iinhoiicclem  44211  preimageiingt  44257  preimaleiinlt  44258  smflimlem2  44307  smflimsuplem5  44357  smflimsuplem7  44359