Theorem eliin 4953

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

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

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 4951

This theorem is referenced by:  iinconst  4959  iuniin  4961  iinssiun  4962  iinss1  4964  ssiinf  5012  iinss  5014  iinss2  5015  iinab  5025  iinun2  5030  iundif2  5031  iindif1  5032  iindif2  5034  iinin2  5035  elriin  5038  iinpw  5063  triin  5223  xpiindi  5792  cnviin  6252  iinpreima  7023  iiner  8738  ixpiin  8874  boxriin  8890  iunocv  21648  hauscmplem  23362  txtube  23596  isfcls  23965  iscmet3  25261  taylfval  26334  suppgsumssiun  33165  zarclsiin  34048  fnemeet1  36579  diaglbN  41425  dibglbN  41536  dihglbcpreN  41670  kelac1  43414  eliind  45425  eliuniin  45452  eliin2f  45457  eliinid  45464  eliuniin2  45473  iinssiin  45482  eliind2  45483  iinssf  45491  iindif2f  45513  allbutfi  45745  meaiininclem  46838  hspdifhsp  46968  iinhoiicclem  47025  preimageiingt  47072  preimaleiinlt  47073  smflimlem2  47124  smflimsuplem5  47176  smflimsuplem7  47178  iineq0  49173  iinxp  49184  iinfsubc  49411