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

Theorem eliin 4900
 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 2898 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 3184 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4898 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3648 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  ∀wral 3125  ∩ ciin 4896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-iin 4898 This theorem is referenced by:  iinconst  4905  iuniin  4907  iinssiun  4908  iinss1  4910  ssiinf  4954  iinss  4956  iinss2  4957  iinab  4966  iinun2  4971  iundif2  4972  iindif1  4973  iindif2  4975  iinin2  4976  elriin  4979  iinpw  5004  triin  5163  xpiindi  5682  cnviin  6113  iinpreima  6813  iiner  8347  ixpiin  8466  boxriin  8482  iunocv  20801  hauscmplem  21990  txtube  22224  isfcls  22593  iscmet3  23876  taylfval  24933  fnemeet1  33722  diaglbN  38227  dibglbN  38338  dihglbcpreN  38472  kelac1  39800  eliind  41488  eliuniin  41520  eliin2f  41525  eliinid  41532  eliuniin2  41540  iinssiin  41549  eliind2  41550  iinssf  41561  allbutfi  41819  meaiininclem  42916  hspdifhsp  43046  iinhoiicclem  43103  preimageiingt  43146  preimaleiinlt  43147  smflimlem2  43196  smflimsuplem5  43246  smflimsuplem7  43248
 Copyright terms: Public domain W3C validator