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

Theorem elintab 4237
Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
inteqab.1  |-  A  e. 
_V
Assertion
Ref Expression
elintab  |-  ( A  e.  |^| { x  | 
ph }  <->  A. x
( ph  ->  A  e.  x ) )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem elintab
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 inteqab.1 . . 3  |-  A  e. 
_V
21elint 4232 . 2  |-  ( A  e.  |^| { x  | 
ph }  <->  A. y
( y  e.  {
x  |  ph }  ->  A  e.  y ) )
3 nfsab1 2461 . . . 4  |-  F/ x  y  e.  { x  |  ph }
4 nfv 1769 . . . 4  |-  F/ x  A  e.  y
53, 4nfim 2023 . . 3  |-  F/ x
( y  e.  {
x  |  ph }  ->  A  e.  y )
6 nfv 1769 . . 3  |-  F/ y ( ph  ->  A  e.  x )
7 eleq1 2537 . . . . 5  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  x  e.  { x  |  ph }
) )
8 abid 2459 . . . . 5  |-  ( x  e.  { x  | 
ph }  <->  ph )
97, 8syl6bb 269 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  ph ) )
10 eleq2 2538 . . . 4  |-  ( y  =  x  ->  ( A  e.  y  <->  A  e.  x ) )
119, 10imbi12d 327 . . 3  |-  ( y  =  x  ->  (
( y  e.  {
x  |  ph }  ->  A  e.  y )  <-> 
( ph  ->  A  e.  x ) ) )
125, 6, 11cbval 2127 . 2  |-  ( A. y ( y  e. 
{ x  |  ph }  ->  A  e.  y )  <->  A. x ( ph  ->  A  e.  x ) )
132, 12bitri 257 1  |-  ( A  e.  |^| { x  | 
ph }  <->  A. x
( ph  ->  A  e.  x ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1450    e. wcel 1904   {cab 2457   _Vcvv 3031   |^|cint 4226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-int 4227
This theorem is referenced by:  elintrab  4238  intmin4  4255  intab  4256  intid  4658  dfom3  8170  dfom5  8173  tc2  8244  dfnn2  10644  brintclab  13142  efgi  17447  efgi2  17453  mclsax  30279  heibor1lem  32205  elmapintab  36273  intabssd  36287  cotrintab  36292  dffrege76  36606
  Copyright terms: Public domain W3C validator