MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eliin Structured version   Visualization version   GIF version

Theorem eliin 4516
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.
StepHypRef Expression
1 eleq1 2687 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 2983 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4514 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3347 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  wral 2909   ciin 4512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-v 3197  df-iin 4514
This theorem is referenced by:  iinconst  4521  iuniin  4522  iinss1  4524  ssiinf  4560  iinss  4562  iinss2  4563  iinab  4572  iinun2  4577  iundif2  4578  iindif2  4580  iinin2  4581  elriin  4584  iinpw  4608  xpiindi  5246  cnviin  5660  iinpreima  6331  iiner  7804  ixpiin  7919  boxriin  7935  iunocv  20006  hauscmplem  21190  txtube  21424  isfcls  21794  iscmet3  23072  taylfval  24094  iinssiun  29349  fnemeet1  32336  diaglbN  36163  dibglbN  36274  dihglbcpreN  36408  kelac1  37452  eliind  39060  eliuniin  39099  eliin2f  39107  eliinid  39114  eliuniin2  39123  iinssiin  39132  eliind2  39133  iinssf  39147  allbutfi  39429  meaiininclem  40463  hspdifhsp  40593  iinhoiicclem  40650  preimageiingt  40693  preimaleiinlt  40694  smflimlem2  40743  smflimsuplem5  40793  smflimsuplem7  40795
  Copyright terms: Public domain W3C validator