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

Theorem elrab 2813
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 2258 . 2  |-  F/_ x A
2 nfcv 2258 . 2  |-  F/_ x B
3 nfv 1493 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 2811 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1316    e. wcel 1465   {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-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rab 2402  df-v 2662
This theorem is referenced by:  elrab3  2814  elrabd  2815  elrab2  2816  ralrab  2818  rexrab  2820  rabsnt  3568  unimax  3740  ssintub  3759  intminss  3766  exmidexmid  4090  exmidsssnc  4096  rabxfrd  4360  ordtri2or2exmidlem  4411  onsucelsucexmidlem1  4413  sefvex  5410  ssimaex  5450  acexmidlem2  5739  elpmg  6526  ssfilem  6737  diffitest  6749  inffiexmid  6768  supubti  6854  suplubti  6855  ctssexmid  6992  exmidonfinlem  7017  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemub  7499  nnindnn  7669  negf1o  8112  apsscn  8377  sup3exmid  8683  nnind  8704  peano2uz2  9126  peano5uzti  9127  dfuzi  9129  uzind  9130  uzind3  9132  eluz1  9298  uzind4  9351  supinfneg  9358  infsupneg  9359  eqreznegel  9374  elixx1  9648  elioo2  9672  elfz1  9763  expcl2lemap  10273  expclzaplem  10285  expclzap  10286  expap0i  10293  expge0  10297  expge1  10298  hashennnuni  10493  shftf  10570  reccn2ap  11050  dvdsdivcl  11475  divalgmod  11551  zsupcl  11567  infssuzex  11569  infssuzcldc  11571  bezoutlemsup  11624  dfgcd2  11629  lcmcllem  11675  lcmledvds  11678  lcmgcdlem  11685  1nprm  11722  1idssfct  11723  isprm2  11725  phicl2  11817  hashdvds  11824  oddennn  11832  evenennn  11833  znnen  11838  ennnfonelemg  11843  ennnfonelemom  11848  istopon  12107  epttop  12186  iscld  12199  isnei  12240  neipsm  12250  iscn  12293  iscnp  12295  txdis1cn  12374  ishmeo  12400  ispsmet  12419  ismet  12440  isxmet  12441  elblps  12486  elbl  12487  xmetxpbl  12604  reopnap  12634  divcnap  12651  elcncf  12656  cdivcncfap  12683  cnopnap  12690  ellimc3apf  12725  limccoap  12743  dvlemap  12745  dvidlemap  12756  dvcnp2cntop  12759  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvcjbr  12768  dvrecap  12773  dveflem  12782  subctctexmid  13123
  Copyright terms: Public domain W3C validator