Theorem eliin 4959

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∩ ciin 4955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-iin 4957

This theorem is used by:  iinconst  4965  iuniin  4967  iinssiun  4968  iinss1  4970  ssiinf  5017  iinss  5019  iinss2  5020  iinab  5030  iinun2  5035  iundif2  5036  iindif1  5039  iindif2  5041  iinin2  5042  elriin  5045  iinpw  5070  triin  5233  xpiindi  5819  cnviin  6288  iinpreima  7066  iiner  8793  ixpiin  8935  boxriin  8951  iunocv  21900  hauscmplem  23637  txtube  23872  isfcls  24241  iscmet3  25527  taylfval  26602  suppgsumssiun  33520  zarclsiin  34389  fnemeet1  36993  diaglbN  41936  dibglbN  42047  dihglbcpreN  42181  kelac1  43912  eliind  45913  eliuniin  45939  eliin2f  45944  eliinid  45951  eliuniin2  45960  iinssiin  45969  eliind2  45970  iinssf  45978  iindif2f  46000  allbutfi  46230  meaiininclem  47322  hspdifhsp  47452  iinhoiicclem  47509  preimageiingt  47556  preimaleiinlt  47557  smflimlem2  47608  smflimsuplem5  47660  smflimsuplem7  47662  iineq0  49756  iinxp  49767  iinfsubc  49992