Theorem eliin 4957

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ∩ ciin 4953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-iin 4955

This theorem is referenced by:  iinconst  4963  iuniin  4965  iinssiun  4966  iinss1  4968  ssiinf  5015  iinss  5017  iinss2  5018  iinab  5028  iinun2  5033  iundif2  5034  iindif1  5037  iindif2  5039  iinin2  5040  elriin  5043  iinpw  5068  triin  5229  xpiindi  5812  cnviin  6277  iinpreima  7054  iiner  8775  ixpiin  8910  boxriin  8926  iunocv  21791  hauscmplem  23524  txtube  23758  isfcls  24127  iscmet3  25413  taylfval  26480  suppgsumssiun  33305  zarclsiin  34178  fnemeet1  36739  diaglbN  41691  dibglbN  41802  dihglbcpreN  41936  kelac1  43652  eliind  45649  eliuniin  45675  eliin2f  45680  eliinid  45687  eliuniin2  45696  iinssiin  45705  eliind2  45706  iinssf  45714  iindif2f  45736  allbutfi  45966  meaiininclem  47058  hspdifhsp  47188  iinhoiicclem  47245  preimageiingt  47292  preimaleiinlt  47293  smflimlem2  47344  smflimsuplem5  47396  smflimsuplem7  47398  iineq0  49449  iinxp  49460  iinfsubc  49687