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

Theorem elrab 2750
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
Hypothesis
Ref Expression
elrab.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
elrab  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Distinct variable groups:    ps, x    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem elrab
StepHypRef Expression
1 nfcv 2220 . 2  |-  F/_ x A
2 nfcv 2220 . 2  |-  F/_ x B
3 nfv 1462 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 2748 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285    e. wcel 1434   {crab 2353
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-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rab 2358  df-v 2604
This theorem is referenced by:  elrab3  2751  elrab2  2752  ralrab  2754  rexrab  2756  rabsnt  3475  unimax  3643  ssintub  3662  intminss  3669  rabxfrd  4227  ordtri2or2exmidlem  4277  onsucelsucexmidlem1  4279  sefvex  5227  ssimaex  5266  acexmidlem2  5540  ssfilem  6410  diffitest  6421  supubti  6471  suplubti  6472  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  nnindnn  7121  negf1o  7553  nnind  8122  peano2uz2  8535  peano5uzti  8536  dfuzi  8538  uzind  8539  uzind3  8541  eluz1  8704  uzind4  8757  supinfneg  8764  infsupneg  8765  eqreznegel  8780  elixx1  8996  elioo2  9020  elfz1  9110  serige0  9570  expcl2lemap  9585  expclzaplem  9597  expclzap  9598  expap0i  9605  expge0  9609  expge1  9610  sizeennnuni  9803  shftf  9856  dvdsdivcl  10395  divalgmod  10471  zsupcl  10487  infssuzex  10489  infssuzcldc  10491  bezoutlemsup  10542  dfgcd2  10547  lcmcllem  10593  lcmledvds  10596  lcmgcdlem  10603  1nprm  10640  1idssfct  10641  isprm2  10643  oddennn  10703  evenennn  10704  znnen  10709
  Copyright terms: Public domain W3C validator