Theorem eliin 4938

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-iin 4936

This theorem is referenced by:  iinconst  4944  iuniin  4946  iinssiun  4947  iinss1  4949  ssiinf  4997  iinss  4999  iinss2  5000  iinab  5010  iinun2  5015  iundif2  5016  iindif1  5017  iindif2  5019  iinin2  5020  elriin  5023  iinpw  5048  triin  5209  xpiindi  5790  cnviin  6250  iinpreima  7021  iiner  8736  ixpiin  8872  boxriin  8888  iunocv  21661  hauscmplem  23371  txtube  23605  isfcls  23974  iscmet3  25260  taylfval  26324  suppgsumssiun  33133  zarclsiin  34015  fnemeet1  36548  diaglbN  41501  dibglbN  41612  dihglbcpreN  41746  kelac1  43491  eliind  45502  eliuniin  45529  eliin2f  45534  eliinid  45541  eliuniin2  45550  iinssiin  45559  eliind2  45560  iinssf  45568  iindif2f  45590  allbutfi  45822  meaiininclem  46914  hspdifhsp  47044  iinhoiicclem  47101  preimageiingt  47148  preimaleiinlt  47149  smflimlem2  47200  smflimsuplem5  47252  smflimsuplem7  47254  iineq0  49295  iinxp  49306  iinfsubc  49533