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

Theorem elrab 2811
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 2256 . 2  |-  F/_ x A
2 nfcv 2256 . 2  |-  F/_ x B
3 nfv 1491 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 2809 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 1314    e. wcel 1463   {crab 2395
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rab 2400  df-v 2660
This theorem is referenced by:  elrab3  2812  elrabd  2813  elrab2  2814  ralrab  2816  rexrab  2818  rabsnt  3566  unimax  3738  ssintub  3757  intminss  3764  exmidexmid  4088  exmidsssnc  4094  rabxfrd  4358  ordtri2or2exmidlem  4409  onsucelsucexmidlem1  4411  sefvex  5408  ssimaex  5448  acexmidlem2  5737  elpmg  6524  ssfilem  6735  diffitest  6747  inffiexmid  6766  supubti  6852  suplubti  6853  ctssexmid  6990  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  suplocexprlemmu  7490  suplocexprlemru  7491  suplocexprlemdisj  7492  suplocexprlemub  7495  nnindnn  7665  negf1o  8108  apsscn  8371  sup3exmid  8672  nnind  8693  peano2uz2  9109  peano5uzti  9110  dfuzi  9112  uzind  9113  uzind3  9115  eluz1  9279  uzind4  9332  supinfneg  9339  infsupneg  9340  eqreznegel  9355  elixx1  9620  elioo2  9644  elfz1  9735  expcl2lemap  10245  expclzaplem  10257  expclzap  10258  expap0i  10265  expge0  10269  expge1  10270  hashennnuni  10465  shftf  10542  reccn2ap  11022  dvdsdivcl  11444  divalgmod  11520  zsupcl  11536  infssuzex  11538  infssuzcldc  11540  bezoutlemsup  11593  dfgcd2  11598  lcmcllem  11644  lcmledvds  11647  lcmgcdlem  11654  1nprm  11691  1idssfct  11692  isprm2  11694  phicl2  11785  hashdvds  11792  oddennn  11800  evenennn  11801  znnen  11806  ennnfonelemg  11811  ennnfonelemom  11816  istopon  12075  epttop  12154  iscld  12167  isnei  12208  neipsm  12218  iscn  12261  iscnp  12263  txdis1cn  12342  ishmeo  12368  ispsmet  12387  ismet  12408  isxmet  12409  elblps  12454  elbl  12455  xmetxpbl  12572  reopnap  12602  divcnap  12619  elcncf  12624  cdivcncfap  12651  cnopnap  12658  ellimc3apf  12681  limccoap  12699  dvlemap  12701  dvidlemap  12712  dvcnp2cntop  12715  dvaddxxbr  12717  dvmulxxbr  12718  dvcoapbr  12723  dvcjbr  12724  dvrecap  12729  dveflem  12738  subctctexmid  13007
  Copyright terms: Public domain W3C validator