Theorem eliin 4995

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3060  ∩ ciin 4991

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-iin 4993

This theorem is referenced by:  iinconst  5000  iuniin  5002  iinssiun  5003  iinss1  5005  ssiinf  5050  iinss  5052  iinss2  5053  iinab  5064  iinun2  5069  iundif2  5070  iindif1  5071  iindif2  5073  iinin2  5074  elriin  5077  iinpw  5102  triin  5275  xpiindi  5827  cnviin  6274  iinpreima  7055  iiner  8766  ixpiin  8901  boxriin  8917  iunocv  21167  hauscmplem  22839  txtube  23073  isfcls  23442  iscmet3  24739  taylfval  25800  zarclsiin  32682  fnemeet1  35055  diaglbN  39731  dibglbN  39842  dihglbcpreN  39976  kelac1  41576  eliind  43529  eliuniin  43559  eliin2f  43564  eliinid  43571  eliuniin2  43580  iinssiin  43589  eliind2  43590  iinssf  43598  iindif2f  43625  allbutfi  43876  meaiininclem  44975  hspdifhsp  45105  iinhoiicclem  45162  preimageiingt  45209  preimaleiinlt  45210  smflimlem2  45261  smflimsuplem5  45313  smflimsuplem7  45315