Theorem eliin 4972

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3051  ∩ ciin 4968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-iin 4970

This theorem is referenced by:  iinconst  4978  iuniin  4980  iinssiun  4981  iinss1  4983  ssiinf  5030  iinss  5032  iinss2  5033  iinab  5044  iinun2  5049  iundif2  5050  iindif1  5051  iindif2  5053  iinin2  5054  elriin  5057  iinpw  5082  triin  5246  xpiindi  5815  cnviin  6275  iinpreima  7058  iiner  8801  ixpiin  8936  boxriin  8952  iunocv  21639  hauscmplem  23342  txtube  23576  isfcls  23945  iscmet3  25243  taylfval  26316  zarclsiin  33848  fnemeet1  36330  diaglbN  41020  dibglbN  41131  dihglbcpreN  41265  kelac1  43034  eliind  45043  eliuniin  45071  eliin2f  45076  eliinid  45083  eliuniin2  45092  iinssiin  45101  eliind2  45102  iinssf  45110  iindif2f  45132  allbutfi  45368  meaiininclem  46463  hspdifhsp  46593  iinhoiicclem  46650  preimageiingt  46697  preimaleiinlt  46698  smflimlem2  46749  smflimsuplem5  46801  smflimsuplem7  46803  iineq0  48746  iinxp  48757  iinfsubc  48973