Theorem eliin 4760

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ∈ wcel 2107  ∀wral 3090  ∩ ciin 4756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-v 3400  df-iin 4758

This theorem is referenced by:  iinconst  4765  iuniin  4766  iinss1  4768  ssiinf  4804  iinss  4806  iinss2  4807  iinab  4816  iinun2  4821  iundif2  4822  iindif2  4824  iinin2  4825  elriin  4828  iinpw  4853  triin  5004  xpiindi  5505  cnviin  5928  iinpreima  6611  iiner  8104  ixpiin  8222  boxriin  8238  iunocv  20435  hauscmplem  21629  txtube  21863  isfcls  22232  iscmet3  23510  taylfval  24561  iinssiun  29956  fnemeet1  32957  diaglbN  37218  dibglbN  37329  dihglbcpreN  37463  kelac1  38606  eliind  40185  eliuniin  40224  eliin2f  40230  eliinid  40237  eliuniin2  40246  iinssiin  40254  eliind2  40255  iinssf  40267  allbutfi  40536  meaiininclem  41641  hspdifhsp  41771  iinhoiicclem  41828  preimageiingt  41871  preimaleiinlt  41872  smflimlem2  41921  smflimsuplem5  41971  smflimsuplem7  41973