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

Theorem elrabi 2810
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 2242 . . 3  |-  ( A  e.  { x  |  ( x  e.  V  /\  ph ) }  <->  E. x
( x  =  A  /\  ( x  e.  V  /\  ph )
) )
2 eleq1 2180 . . . . . 6  |-  ( x  =  A  ->  (
x  e.  V  <->  A  e.  V ) )
32anbi1d 460 . . . . 5  |-  ( x  =  A  ->  (
( x  e.  V  /\  ph )  <->  ( A  e.  V  /\  ph )
) )
43simprbda 380 . . . 4  |-  ( ( x  =  A  /\  ( x  e.  V  /\  ph ) )  ->  A  e.  V )
54exlimiv 1562 . . 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 2402 . 2  |-  { x  e.  V  |  ph }  =  { x  |  ( x  e.  V  /\  ph ) }
86, 7eleq2s 2212 1  |-  ( A  e.  { x  e.  V  |  ph }  ->  A  e.  V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1316   E.wex 1453    e. wcel 1465   {cab 2103   {crab 2397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-rab 2402
This theorem is referenced by:  ordtriexmidlem  4405  ordtri2or2exmidlem  4411  onsucelsucexmidlem  4414  ordsoexmid  4447  reg3exmidlemwe  4463  elfvmptrab1  5483  acexmidlemcase  5737  ssfirab  6790  exmidonfinlem  7017  genpelvl  7288  genpelvu  7289  suplocsrlempr  7583  nnindnn  7669  sup3exmid  8683  nnind  8704  supinfneg  9358  infsupneg  9359  supminfex  9360  ublbneg  9373  hashinfuni  10491  zsupcllemstep  11565  infssuzex  11569  infssuzledc  11570  bezoutlemsup  11624  lcmgcdlem  11685  oddennn  11832  evenennn  11833  znnen  11838  ennnfonelemg  11843  txdis1cn  12374  reopnap  12634  divcnap  12651  limccl  12724  dvlemap  12745  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvcjbr  12768  dvrecap  12773  dveflem  12782
  Copyright terms: Public domain W3C validator