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

Theorem elint2 4295
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 4294 . 2  |-  ( A  e.  |^| B  <->  A. x
( x  e.  B  ->  A  e.  x ) )
3 df-ral 2812 . 2  |-  ( A. x  e.  B  A  e.  x  <->  A. x ( x  e.  B  ->  A  e.  x ) )
42, 3bitr4i 252 1  |-  ( A  e.  |^| B  <->  A. x  e.  B  A  e.  x )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1393    e. wcel 1819   A.wral 2807   _Vcvv 3109   |^|cint 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-int 4289
This theorem is referenced by:  elintg  4296  ssint  4304  intssuni  4311  iinuni  4419  trint  4565  trintss  4566  onint  6629  intwun  9130  inttsk  9169  intgru  9209  subgint  16351  subrgint  17577  lssintcl  17736  toponmre  19720  alexsubALTlem3  20674  shintcli  26373  chintcli  26375  fin2so  30202  intidl  30588  mzpincl  30828  elimaint  37865  elintima  37866
  Copyright terms: Public domain W3C validator