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

Theorem elint2 3885
Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
Hypothesis
Ref Expression
elint2.1  |-  A  e. 
_V
Assertion
Ref Expression
elint2  |-  ( A  e.  |^| B  <->  A. x  e.  B  A  e.  x )
Distinct variable groups:    x, A    x, B

Proof of Theorem elint2
StepHypRef Expression
1 elint2.1 . . 3  |-  A  e. 
_V
21elint 3884 . 2  |-  ( A  e.  |^| B  <->  A. x
( x  e.  B  ->  A  e.  x ) )
3 df-ral 2561 . 2  |-  ( A. x  e.  B  A  e.  x  <->  A. x ( x  e.  B  ->  A  e.  x ) )
42, 3bitr4i 243 1  |-  ( A  e.  |^| B  <->  A. x  e.  B  A  e.  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    e. wcel 1696   A.wral 2556   _Vcvv 2801   |^|cint 3878
This theorem is referenced by:  elintg  3886  ssint  3894  intssuni  3900  iinuni  4001  trint  4144  trintss  4145  onint  4602  intwun  8373  inttsk  8412  intgru  8452  subgint  14657  subrgint  15583  lssintcl  15737  toponmre  16846  alexsubALTlem3  17759  shintcli  21924  chintcli  21926  intidl  26757  mzpincl  26915
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-int 3879
  Copyright terms: Public domain W3C validator