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

Theorem elrab 2762
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 2225 . 2  |-  F/_ x A
2 nfcv 2225 . 2  |-  F/_ x B
3 nfv 1464 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 2760 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 1287    e. wcel 1436   {crab 2359
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rab 2364  df-v 2617
This theorem is referenced by:  elrab3  2763  elrabd  2764  elrab2  2765  ralrab  2767  rexrab  2769  rabsnt  3502  unimax  3672  ssintub  3691  intminss  3698  exmidexmid  4007  rabxfrd  4267  ordtri2or2exmidlem  4317  onsucelsucexmidlem1  4319  sefvex  5291  ssimaex  5330  acexmidlem2  5612  elpmg  6375  ssfilem  6545  diffitest  6557  inffiexmid  6576  supubti  6641  suplubti  6642  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  nnindnn  7375  negf1o  7807  nnind  8376  peano2uz2  8789  peano5uzti  8790  dfuzi  8792  uzind  8793  uzind3  8795  eluz1  8958  uzind4  9011  supinfneg  9018  infsupneg  9019  eqreznegel  9034  elixx1  9250  elioo2  9274  elfz1  9364  expcl2lemap  9887  expclzaplem  9899  expclzap  9900  expap0i  9907  expge0  9911  expge1  9912  hashennnuni  10105  shftf  10182  dvdsdivcl  10776  divalgmod  10852  zsupcl  10868  infssuzex  10870  infssuzcldc  10872  bezoutlemsup  10923  dfgcd2  10928  lcmcllem  10974  lcmledvds  10977  lcmgcdlem  10984  1nprm  11021  1idssfct  11022  isprm2  11024  phicl2  11115  hashdvds  11122  oddennn  11130  evenennn  11131  znnen  11136
  Copyright terms: Public domain W3C validator