Theorem eliin 4525

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∩ ciin 4521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-iin 4523

This theorem is referenced by:  iinconst  4530  iuniin  4531  iinss1  4533  ssiinf  4569  iinss  4571  iinss2  4572  iinab  4581  iinun2  4586  iundif2  4587  iindif2  4589  iinin2  4590  elriin  4593  iinpw  4617  xpiindi  5257  cnviin  5672  iinpreima  6345  iiner  7819  ixpiin  7934  boxriin  7950  iunocv  20025  hauscmplem  21209  txtube  21443  isfcls  21813  iscmet3  23091  taylfval  24113  iinssiun  29377  fnemeet1  32361  diaglbN  36344  dibglbN  36455  dihglbcpreN  36589  kelac1  37633  eliind  39240  eliuniin  39279  eliin2f  39287  eliinid  39294  eliuniin2  39303  iinssiin  39312  eliind2  39313  iinssf  39327  allbutfi  39616  meaiininclem  40700  hspdifhsp  40830  iinhoiicclem  40887  preimageiingt  40930  preimaleiinlt  40931  smflimlem2  40980  smflimsuplem5  41030  smflimsuplem7  41032