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

Theorem elrabi 2804
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 2237 . . 3  |-  ( A  e.  { x  |  ( x  e.  V  /\  ph ) }  <->  E. x
( x  =  A  /\  ( x  e.  V  /\  ph )
) )
2 eleq1 2175 . . . . . 6  |-  ( x  =  A  ->  (
x  e.  V  <->  A  e.  V ) )
32anbi1d 458 . . . . 5  |-  ( x  =  A  ->  (
( x  e.  V  /\  ph )  <->  ( A  e.  V  /\  ph )
) )
43simprbda 378 . . . 4  |-  ( ( x  =  A  /\  ( x  e.  V  /\  ph ) )  ->  A  e.  V )
54exlimiv 1558 . . 3  |-  ( E. x ( x  =  A  /\  ( x  e.  V  /\  ph ) )  ->  A  e.  V )
61, 5sylbi 120 . 2  |-  ( A  e.  { x  |  ( x  e.  V  /\  ph ) }  ->  A  e.  V )
7 df-rab 2397 . 2  |-  { x  e.  V  |  ph }  =  { x  |  ( x  e.  V  /\  ph ) }
86, 7eleq2s 2207 1  |-  ( A  e.  { x  e.  V  |  ph }  ->  A  e.  V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1312   E.wex 1449    e. wcel 1461   {cab 2099   {crab 2392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-rab 2397
This theorem is referenced by:  ordtriexmidlem  4393  ordtri2or2exmidlem  4399  onsucelsucexmidlem  4402  ordsoexmid  4435  reg3exmidlemwe  4451  elfvmptrab1  5467  acexmidlemcase  5721  ssfirab  6771  genpelvl  7261  genpelvu  7262  nnindnn  7621  sup3exmid  8618  nnind  8639  supinfneg  9285  infsupneg  9286  supminfex  9287  ublbneg  9300  hashinfuni  10409  zsupcllemstep  11479  infssuzex  11483  infssuzledc  11484  bezoutlemsup  11536  lcmgcdlem  11597  oddennn  11743  evenennn  11744  znnen  11749  ennnfonelemg  11754  txdis1cn  12282  divcnap  12534  limccl  12577  dvlemap  12597
  Copyright terms: Public domain W3C validator