ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elrabi Unicode version

Theorem elrabi 2766
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
Assertion
Ref Expression
elrabi  |-  ( A  e.  { x  e.  V  |  ph }  ->  A  e.  V )
Distinct variable groups:    x, A    x, V
Allowed substitution hint:    ph( x)

Proof of Theorem elrabi
StepHypRef Expression
1 clelab 2212 . . 3  |-  ( A  e.  { x  |  ( x  e.  V  /\  ph ) }  <->  E. x
( x  =  A  /\  ( x  e.  V  /\  ph )
) )
2 eleq1 2150 . . . . . 6  |-  ( x  =  A  ->  (
x  e.  V  <->  A  e.  V ) )
32anbi1d 453 . . . . 5  |-  ( x  =  A  ->  (
( x  e.  V  /\  ph )  <->  ( A  e.  V  /\  ph )
) )
43simprbda 375 . . . 4  |-  ( ( x  =  A  /\  ( x  e.  V  /\  ph ) )  ->  A  e.  V )
54exlimiv 1534 . . 3  |-  ( E. x ( x  =  A  /\  ( x  e.  V  /\  ph ) )  ->  A  e.  V )
61, 5sylbi 119 . 2  |-  ( A  e.  { x  |  ( x  e.  V  /\  ph ) }  ->  A  e.  V )
7 df-rab 2368 . 2  |-  { x  e.  V  |  ph }  =  { x  |  ( x  e.  V  /\  ph ) }
86, 7eleq2s 2182 1  |-  ( A  e.  { x  e.  V  |  ph }  ->  A  e.  V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1289   E.wex 1426    e. wcel 1438   {cab 2074   {crab 2363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-rab 2368
This theorem is referenced by:  ordtriexmidlem  4326  ordtri2or2exmidlem  4332  onsucelsucexmidlem  4335  ordsoexmid  4368  reg3exmidlemwe  4384  acexmidlemcase  5629  ssfirab  6622  genpelvl  7050  genpelvu  7051  nnindnn  7407  nnind  8410  supinfneg  9052  infsupneg  9053  supminfex  9054  ublbneg  9067  hashinfuni  10150  zsupcllemstep  11023  infssuzex  11027  infssuzledc  11028  bezoutlemsup  11080  lcmgcdlem  11141  oddennn  11287  evenennn  11288  znnen  11293
  Copyright terms: Public domain W3C validator