Theorem eliin 4939

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∩ ciin 4935

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-iin 4937

This theorem is referenced by:  iinconst  4945  iuniin  4947  iinssiun  4948  iinss1  4950  ssiinf  4998  iinss  5000  iinss2  5001  iinab  5011  iinun2  5016  iundif2  5017  iindif1  5018  iindif2  5020  iinin2  5021  elriin  5024  iinpw  5049  triin  5209  xpiindi  5784  cnviin  6244  iinpreima  7015  iiner  8729  ixpiin  8865  boxriin  8881  iunocv  21671  hauscmplem  23381  txtube  23615  isfcls  23984  iscmet3  25270  taylfval  26335  suppgsumssiun  33148  zarclsiin  34031  fnemeet1  36564  diaglbN  41515  dibglbN  41626  dihglbcpreN  41760  kelac1  43509  eliind  45520  eliuniin  45547  eliin2f  45552  eliinid  45559  eliuniin2  45568  iinssiin  45577  eliind2  45578  iinssf  45586  iindif2f  45608  allbutfi  45840  meaiininclem  46932  hspdifhsp  47062  iinhoiicclem  47119  preimageiingt  47166  preimaleiinlt  47167  smflimlem2  47218  smflimsuplem5  47270  smflimsuplem7  47272  iineq0  49307  iinxp  49318  iinfsubc  49545