Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elintab Unicode version

Theorem elintab 4297
 Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
inteqab.1
Assertion
Ref Expression
elintab
Distinct variable group:   ,

Proof of Theorem elintab
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 inteqab.1 . . 3
21elint 4292 . 2
3 nfsab1 2446 . . . 4
4 nfv 1707 . . . 4
53, 4nfim 1920 . . 3
6 nfv 1707 . . 3
7 eleq1 2529 . . . . 5
8 abid 2444 . . . . 5
97, 8syl6bb 261 . . . 4
10 eleq2 2530 . . . 4
119, 10imbi12d 320 . . 3
125, 6, 11cbval 2021 . 2
132, 12bitri 249 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  {cab 2442   cvv 3109  |^|cint 4286 This theorem is referenced by:  elintrab  4298  intmin4  4316  intab  4317  intid  4710  dfom3  8085  dfom5  8088  tc2  8194  dfnn2  10574  efgi  16737  efgi2  16743  mclsax  28929  heibor1lem  30305  brintclab  37763 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-int 4287
 Copyright terms: Public domain W3C validator