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

Theorem elrab2 2772
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
Hypotheses
Ref Expression
elrab2.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
elrab2.2  |-  C  =  { x  e.  B  |  ph }
Assertion
Ref Expression
elrab2  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Distinct variable groups:    ps, x    x, A    x, B
Allowed substitution hints:    ph( x)    C( x)

Proof of Theorem elrab2
StepHypRef Expression
1 elrab2.2 . . 3  |-  C  =  { x  e.  B  |  ph }
21eleq2i 2154 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 2769 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 182 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1289    e. wcel 1438   {crab 2363
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rab 2368  df-v 2621
This theorem is referenced by:  elrabsf  2875  pwnss  3986  regexmidlemm  4338  regexmidlem1  4339  reg2exmidlema  4340  tfis  4388  infnninf  6784  nnnninf  6785  ltexprlemell  7136  ltexprlemelu  7137  cauappcvgprlemm  7183  cauappcvgprlemopl  7184  cauappcvgprlemlol  7185  cauappcvgprlemopu  7186  cauappcvgprlemupu  7187  cauappcvgprlemdisj  7189  cauappcvgprlemloc  7190  cauappcvgprlemladdfu  7192  cauappcvgprlemladdfl  7193  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  cauappcvgprlem2  7198  caucvgprlemm  7206  caucvgprlemopl  7207  caucvgprlemlol  7208  caucvgprlemopu  7209  caucvgprlemupu  7210  caucvgprlemdisj  7212  caucvgprlemloc  7213  caucvgprlemladdfu  7215  caucvgprlem2  7218  caucvgprprlemell  7223  caucvgprprlemelu  7224  caucvgprprlemml  7232  caucvgprprlemmu  7233  caucvgprprlemexbt  7244  caucvgprprlem2  7248  elz  8722  elrp  9105  repos  9357  isprm  11184  oddpwdc  11245  sqpweven  11246  2sqpwodd  11247  phimullem  11294  hashgcdlem  11296  0nninf  11550  nninff  11551  nnsf  11552  peano4nninf  11553  nninfalllemn  11555  nninfalllem1  11556  nninfself  11562  qdencn  11572
  Copyright terms: Public domain W3C validator