Theorem eliin 4926

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∩ ciin 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-iin 4924

This theorem is referenced by:  iinconst  4931  iuniin  4933  iinssiun  4934  iinss1  4936  ssiinf  4980  iinss  4982  iinss2  4983  iinab  4993  iinun2  4998  iundif2  4999  iindif1  5000  iindif2  5002  iinin2  5003  elriin  5006  iinpw  5031  triin  5202  xpiindi  5733  cnviin  6178  iinpreima  6928  iiner  8536  ixpiin  8670  boxriin  8686  iunocv  20798  hauscmplem  22465  txtube  22699  isfcls  23068  iscmet3  24362  taylfval  25423  zarclsiin  31723  fnemeet1  34482  diaglbN  38996  dibglbN  39107  dihglbcpreN  39241  kelac1  40804  eliind  42508  eliuniin  42538  eliin2f  42543  eliinid  42550  eliuniin2  42558  iinssiin  42567  eliind2  42568  iinssf  42576  allbutfi  42823  meaiininclem  43914  hspdifhsp  44044  iinhoiicclem  44101  preimageiingt  44144  preimaleiinlt  44145  smflimlem2  44194  smflimsuplem5  44244  smflimsuplem7  44246